diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-17 18:09:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-19 18:52:13 +0100 |
| commit | 090fffa57b2235f70d4355f5dc85d73fa2634655 (patch) | |
| tree | d07b76c4f97d2c1266563ccdb8f5ee1c86143054 /pretyping/evd.mli | |
| parent | 51c8b16816ad0e9bdfaab0314fa6a0db5f4528f5 (diff) | |
Option -type-in-type continued (deactivate test for inferred sort of
inductive types + deactivate test for equality of sort + deactivate
the check that the constraints Prop/Set <= Type are declared).
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 6c7ef2168..df5269d34 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -504,7 +504,7 @@ val normalize_universe : evar_map -> Univ.universe -> Univ.universe val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map -val set_eq_sort : evar_map -> sorts -> sorts -> evar_map +val set_eq_sort : env -> evar_map -> sorts -> sorts -> evar_map val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map |