Prop.expose: relax type

Reviewed By: jeremydubreil

Differential Revision: D8397706

fbshipit-source-id: 21606ea
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent f88fe8fc3b
commit 2b77c67df5

@ -95,7 +95,7 @@ include Core
(** {2 Basic Functions for Propositions} *)
let expose (p: normal t) : exposed t = Obj.magic p
let expose (p: _ t) : exposed t = Obj.magic p
let expose_sorted (p: sorted t) : exposed t = Obj.magic p

@ -167,7 +167,7 @@ val sigma_normalize_prop : Tenv.t -> 'a t -> hpred list -> hpred list
val normalize : Tenv.t -> exposed t -> normal t
(** normalize a prop *)
val expose : normal t -> exposed t
val expose : _ t -> exposed t
(** expose a prop, no-op used to instantiate the sub-type relation *)
(** {2 Compaction} *)

Loading…
Cancel
Save