diff options
| author | Matthieu Sozeau | 2014-07-14 19:16:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-14 19:18:42 +0200 |
| commit | 7319524e236545c1b7b799950babbb4886415360 (patch) | |
| tree | 4cc3f708205d0e4bb20c1443175ef83f3421f79d | |
| parent | 7f73c09a6031578a1531fade2752b6e99655cba0 (diff) | |
Add interface function to replace new_Type ()
| -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 |