From 86c6649382bb9e42281ffe956c627c6d3987559b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 30 May 2014 21:55:24 +0200 Subject: - Force every universe level to be >= Prop, so one cannot "go under" it anymore. - Finish the change to level-to-level substitutions, in the checker. --- checker/term.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/term.mli') diff --git a/checker/term.mli b/checker/term.mli index cf488f536..5e98885fa 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -55,4 +55,4 @@ val eq_constr : constr -> constr -> bool val subst_univs_constr : Univ.universe_subst -> constr -> constr val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr -val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context +val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_context -- cgit v1.2.3