1 files changed, 10 insertions, 0 deletions
diff --git a/engine/sigma.ml b/engine/sigma.ml
index e6189e29ce..e3e83b6024 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 }