diff options
| -rw-r--r-- | pretyping/evarutil.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 3 |
2 files changed, 11 insertions, 0 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 7fa6f46fbd..d6e8a96606 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -382,6 +382,14 @@ let e_new_type_evar evdref ?src ?filter rigid env = evdref := evd'; c +let new_Type ?(rigid=Evd.univ_flexible) env evd = + let evd', s = new_sort_variable rigid evd in + evd', mkSort s + +let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = + let evd', s = new_sort_variable rigid !evdref in + evdref := evd'; mkSort s + (* The same using side-effect *) let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ?store ty = let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ?store ty in diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index c0708aa85e..3876b0d3e0 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -45,6 +45,9 @@ val new_type_evar : val e_new_type_evar : evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> env -> constr * sorts +val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr +val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr + (** Polymorphic constants *) val new_global : evar_map -> Globnames.global_reference -> evar_map * constr |