diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/sigma.ml | 12 | ||||
| -rw-r--r-- | engine/sigma.mli | 6 |
2 files changed, 18 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, ()) diff --git a/engine/sigma.mli b/engine/sigma.mli index 6ac56bb3e2..cb948dba59 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -66,6 +66,12 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) +val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env -> + 'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma +val fresh_constant_instance : + Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma +val fresh_inductive_instance : + Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma val fresh_constructor_instance : Environ.env -> 'r t -> constructor -> (pconstructor, 'r) sigma |