fixed kernel bug (de Bruijn) + test-suite

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11646 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 26 insertions, 3 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 918a32c95..8024ae266 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -683,7 +683,8 @@ let check_one_fix renv recpos def =
                     List.iter (check_rec_call renv) l
                 | Some c ->
                     try List.iter (check_rec_call renv) l
-                    with FixGuardError _ -> check_rec_call renv (applist(c,l))
+                    with FixGuardError _ ->
+                      check_rec_call renv (applist(lift p c,l))
               end
 
         | Case (ci,p,c_0,lrest) ->
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index 46208c297..7e07a9058 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -8,3 +8,14 @@
 
 Fixpoint F (n:nat) : False := F (match F n with end).
 
+(* de Bruijn mix-up *)
+(* If accepted, Eval compute in f 0. loops *)
+Definition f :=
+  let f (f1 f2:nat->nat) := f1 in
+  let _ := 0 in
+  let _ := 0 in
+  let g (f1 f2:nat->nat) := f2 in
+  let h := f in (* h = Rel 4 *)
+  fix F (n:nat) : nat :=
+  h F S n. (* here Rel 4 = g *)
+  
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 54b03b3eb..b08ffcc32 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -102,8 +102,8 @@ Abort.
 
 (* Check non-regression of bug #1968 *)
 
-Inductive foo : option nat -> Prop := Foo : forall t, foo (Some t).
-Goal forall o, foo o -> 0 = 1.
+Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t).
+Goal forall o, foo2 o -> 0 = 1.
 intros.
 eapply trans_eq. 
 inversion H.
diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v
new file mode 100644
index 000000000..b9181d430
--- /dev/null
+++ b/test-suite/success/guard.v
@@ -0,0 +1,11 @@
+(* Specific tests about guard condition *)
+
+(* f must unfold to x, not F (de Bruijn mix-up!) *)
+Check let x (f:nat->nat) k := f k in
+      fun (y z:nat->nat) =>
+      let f:=x in (* f := Rel 3 *)
+      fix F (n:nat) : nat :=
+        match n with
+        | 0 => 0
+        | S k => f F k (* here Rel 3 = F ! *)
+        end.