Removing some goal unsafeness in inductive schemes.

1 files changed, 12 insertions, 0 deletions

diff --git a/engine/sigma.ml b/engine/sigma.ml
index e3e83b6024..e886b0d1e7 100644
--- a/engine/sigma.ml
+++ b/engine/sigma.ml
@@ -36,6 +36,18 @@ let new_evar sigma ?naming info =
 let define evk c sigma =
   Sigma ((), Evd.define evk c sigma, ())
 
+let fresh_sort_in_family ?rigid env sigma s =
+  let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in
+  Sigma (s, sigma, ())
+
+let fresh_constant_instance env sigma cst =
+  let (sigma, cst) = Evd.fresh_constant_instance env sigma cst in
+  Sigma (cst, sigma, ())
+
+let fresh_inductive_instance env sigma ind =
+  let (sigma, ind) = Evd.fresh_inductive_instance env sigma ind in
+  Sigma (ind, sigma, ())
+
 let fresh_constructor_instance env sigma pc =
   let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in
   Sigma (c, sigma, ())