From 6a3623430870ee1998c172c362bc60591fc908ee Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 26 Aug 2007 17:34:47 +0000
Subject: Fix de Bruijn bug in wf definitions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10096 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/subtac_command.ml | 7 ++++---
 contrib/subtac/test/Mutind.v     | 4 ++--
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b9c25f2074..9d8fdf3e6a 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -242,11 +242,12 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let intern_arity = it_mkProd_or_LetIn top_arity after in
     (try trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++ str "Top arity: " ++ my_print_constr top_env top_arity);
        trace (str "Before lifting arity: " ++ my_print_constr env top_arity) with _ -> ());
-  (* Top arity is in top_env = after :: arg :: before *)
-(*   let intern_arity' = liftn 1 (succ after_length) top_arity in (\* arity in after :: wfarg :: arg :: before *\) *)
+  (* Top arity is in top_env = arg :: before *)
+  let intern_arity = liftn 2 1 intern_arity in
+  (* arity in something :: wfarg :: arg :: before were what refered to arg now refers to something *)
 (*       (try trace (str "projection: " "After lifting arity: " ++ my_print_constr env intern_arity' ++ spc ()); *)
 (* 	 trace (str "Intern env: " ++ prr intern_bl ++ str "intern_arity': " ++ my_print_constr _intern_env intern_arity') with _ -> ()); *)
-  let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for arg *)
+  let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for something *)
   (try trace (str "Top arity after subst: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ());
 (*   let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *)
 (*   (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *)
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index 22ecdc94b6..c2ee4595d0 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,10 +1,10 @@
 Require Import List.
-Program Fixpoint f (a : nat) : { x : nat | x > 0 } := 
+Program Fixpoint f a : { x : nat | x > 0 } := 
   match a with
   | 0 => 1
   | S a' => g a a'
   end
-with g (a b : nat) { struct b } : { x : nat | x > 0 } := 
+with g a b { struct b } : { x : nat | x > 0 } := 
   match b with
   | 0 => 1
   | S b' => f b'
-- 
cgit v1.2.3