diff options
| author | Matthieu Sozeau | 2016-06-29 11:55:31 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-29 11:55:31 +0200 |
| commit | 5e979cf6020eea9fa0feaa77c7436a29443e35db (patch) | |
| tree | 7f2d28d1bfb9dfb72788b434ecada5603afecb57 /engine/evd.mli | |
| parent | 58b6784fee71a16719bc4f268dc42830c06a5c63 (diff) | |
| parent | 40ee96a0392fbc0945c48b5b134aa1be36f86225 (diff) | |
Merge branch 'bug4527' into trunk
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index df491c27b4..d6cf83525c 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -511,6 +511,7 @@ val normalize_evar_universe_context : evar_universe_context -> val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts + val add_global_univ : evar_map -> Univ.Level.t -> evar_map val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map @@ -568,8 +569,8 @@ val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_ val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor -val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> - Globnames.global_reference -> evar_map * constr +val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> + evar_map -> Globnames.global_reference -> evar_map * constr (******************************************************************** Conversion w.r.t. an evar map, not unifying universes. See |