From d6898781f9cd52ac36a4891d7b169ddab7b8af50 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 2 May 2017 19:53:05 +0200 Subject: Correct coqchk reduction --- checker/term.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'checker/term.mli') diff --git a/checker/term.mli b/checker/term.mli index 6b026d056..ccf5b59e0 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -33,6 +33,8 @@ val rel_context_length : rel_context -> int val rel_context_nhyps : rel_context -> int val fold_rel_context : (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a +val fold_rel_context_outside : + (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration val map_rel_context : (constr -> constr) -> rel_context -> rel_context val extended_rel_list : int -> rel_context -> constr list @@ -55,3 +57,4 @@ val eq_constr : constr -> constr -> bool (** Instance substitution for polymorphism. *) val subst_instance_constr : Univ.universe_instance -> constr -> constr val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context +val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr -- cgit v1.2.3