From 029854c7f0c10caf0c26b1e3d73ae011c54ac80e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 19 Jan 2014 02:06:19 +0100
Subject: Fixing checker compilation, which was broken by the following commit:

05d5f8b9065b0f5e0349cf3d39dd62ab99f30369
---
 checker/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/inductive.ml')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index c00a6c5dd..1130c5e03 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -295,7 +295,7 @@ let is_correct_arity env c (p,pj) ind specif params =
 	  check_allowed_sort (family_of_sort s') specif;
 	  false
       | _, (_,Some _,_ as d)::ar' ->
-	 srec (push_rel d env) (lift 1 pt') ar' u
+	 srec (push_rel d env) (lift 1 pt') ar'
       | _ ->
 	  raise (LocalArity None)
   in
-- 
cgit v1.2.3