From 4f041384cb27f0d24fa14b272884b4b7f69cacbe Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 15 Feb 2016 11:55:43 +0100 Subject: CLEANUP: Simplifying the changes done in "kernel/*" ... ... ... ... ... ... ... ... ... ... ... ... ... ... --- kernel/inductive.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ca29d83f6..229508ea3 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -319,7 +319,7 @@ let is_correct_arity env c pj ind specif params = let () = try conv env a1 a1' with NotConvertible -> raise (LocalArity None) in - srec (push_rel (LocalAssum (na1,a1)) env) t ar' + srec (push_rel (LocalAssum (na1,a1)) env) t ar' (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) let env' = push_rel (LocalAssum (na1,a1)) env in -- cgit v1.2.3