From 090fffa57b2235f70d4355f5dc85d73fa2634655 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 17 Nov 2014 18:09:48 +0100 Subject: 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). --- pretyping/evd.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/evd.mli') 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 -- cgit v1.2.3