From a51d94e77bd352522744da4dbdbf98b36c19631e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 10 Apr 2014 20:16:56 -0400
Subject: Fix guard condition for nested cofixpoints in checker.

---
 checker/inductive.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 1130c5e03f..40a9bc316f 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -891,12 +891,12 @@ let check_one_cofix env nbfix def deftype =
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
 
 	| CoFix (j,(_,varit,vdefs as recdef)) ->
-            if (List.for_all (noccur_with_meta n nbfix) args)
+            if List.for_all (noccur_with_meta n nbfix) args
             then
-              let nbfix = Array.length vdefs in
-	      if (Array.for_all (noccur_with_meta n nbfix) varit) then
+	      if Array.for_all (noccur_with_meta n nbfix) varit then
+		let nbfix = Array.length vdefs in
 		let env' = push_rec_types recdef env in
-		(Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs;
+		(Array.iter (check_rec_call env' alreadygrd (n+nbfix) vlra) vdefs;
 		 List.iter (check_rec_call env alreadygrd n vlra) args)
               else
 		raise (CoFixGuardError (env,RecCallInTypeOfDef c))
-- 
cgit v1.2.3