Removing some unsafe uses of monotonicity.

2 files changed, 26 insertions, 0 deletions

diff --git a/engine/sigma.ml b/engine/sigma.ml
index e6189e29c..e3e83b602 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -23,6 +23,8 @@ let lift_evar evk () = evk
 let to_evar_map evd = evd
 let to_evar evk = evk
 
+let here x s = Sigma (x, s, ())
+
 (** API *)
 
 type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
@@ -34,6 +36,14 @@ let new_evar sigma ?naming info =
 let define evk c sigma =
   Sigma ((), Evd.define evk c sigma, ())
 
+let fresh_constructor_instance env sigma pc =
+  let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in
+  Sigma (c, sigma, ())
+
+let fresh_global ?rigid ?names env sigma r =
+  let (sigma, c) = Evd.fresh_global ?rigid ?names env sigma r in
+  Sigma (c, sigma, ())
+
 (** Run *)
 
 type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
diff --git a/engine/sigma.mli b/engine/sigma.mli
index f4c47e08c..6ac56bb3e 100644
--- a/engine/sigma.mli
+++ b/engine/sigma.mli
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
+open Constr
+
 (** Monotonous state enforced by typing.
 
     This module allows to constrain uses of evarmaps in a monotonous fashion,
@@ -37,6 +40,11 @@ type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
 type 'r evar
 (** Stage-indexed evars *)
 
+(** {5 Constructors} *)
+
+val here : 'a -> 'r t -> ('a, 'r) sigma
+(** [here x s] is a shorthand for [Sigma (x, s, refl)] *)
+
 (** {5 Postponing} *)
 
 val lift_evar : 'r evar -> ('r, 's) le -> 's evar
@@ -56,6 +64,14 @@ val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr ->
 
 val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
 
+(** Polymorphic universes *)
+
+val fresh_constructor_instance : Environ.env -> 'r t -> constructor ->
+  (pconstructor, 'r) sigma
+
+val fresh_global : ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
+  'r t -> Globnames.global_reference -> (constr, 'r) sigma
+
 (** FILLME *)
 
 (** {5 Run} *)