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/sigma.mli | |
| parent | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (diff) | |
Removing some goal unsafeness in inductive schemes.
Diffstat (limited to 'engine/sigma.mli')
| -rw-r--r-- | engine/sigma.mli | 6 |
1 files changed, 6 insertions, 0 deletions
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 |