From 9f81e2c360c2be764e71d21ed7c266ee6e8a88c5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 10 Apr 2014 20:05:26 -0400
Subject: Fix guard condition for nested cofixpoints.

There were actually two problems, one of them being clearly unsound.
To make sure that this does not show up somewhere else in the code, it would
be better to resort to an abstraction keeping in sync the environment and the
De Bruijn index of the current cofixpoints, like guard_env does for fixpoints.
---
 kernel/inductive.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index abc6ba4dfb..c0857566df 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -916,12 +916,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