diff options
| author | msozeau | 2007-08-26 17:34:47 +0000 |
|---|---|---|
| committer | msozeau | 2007-08-26 17:34:47 +0000 |
| commit | 6a3623430870ee1998c172c362bc60591fc908ee (patch) | |
| tree | 3541ad74d7de7f07b5fac7625ebd35d52ce9a9c6 | |
| parent | 9d8825bd03f647dc304d6fd36effd80ae3214631 (diff) | |
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
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 7 | ||||
| -rw-r--r-- | 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' |