diff options
| author | Pierre-Marie Pédrot | 2015-10-29 18:18:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-29 19:03:38 +0100 |
| commit | f02f64a21863ce03f2da4ff04cd003051f96801f (patch) | |
| tree | 601fded539120c931b4ece1cff9d0790bdd82fea /engine | |
| parent | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (diff) | |
Removing some goal unsafeness in inductive schemes.
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 |