Fix wf bug from F. Besson and work on ineqs generation.

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

2 files changed, 20 insertions, 17 deletions

diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 72bb80aa6..7e18e58a0 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1698,26 +1698,29 @@ let rec is_included x y =
 	if i = i' then List.for_all2 is_included args args'
 	else false
 
-let build_ineqs prevpatterns pats liftsign patargs =
+(* liftsign is the current pattern's signature length *)
+let build_ineqs prevpatterns pats liftsign =
   let _tomatchs = List.length pats in
   let diffs = 
     List.fold_left 
       (fun c eqnpats -> 
 	 let acc = List.fold_left2
-	   (fun acc (ppat_sign, ppat_c, ppat_ty, (ppat_eqs, ppat_arity), ppat) curpat ->
+	   (fun acc (ppat_sign, ppat_c, ppat_ty, (ppat_eqs, ppat_arity), ppat) 
+	      (curpat_sign, curpat_c, curpat_ty, (curpat_eqs, curpat_arity), curpat) ->
 	      match acc with
 		  None -> None
 		| Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *)
 		    if is_included curpat ppat then
-		      let lens = List.length ppat_sign in
-		      let len' = lens + len in
+		      let lens = List.length ppat_sign in (* Length of previous pattern's signature *)
+		      let len' = lens + len in (* Accumulated length of previous pattern's signatures *)
 		      let acc = 
-			(lift_rel_context len ppat_sign @ sign, 
+			(lift_rel_context len ppat_sign @ sign, (* Jump over previous prevpat signs *)
 			 len',
-			 succ n,
+			 succ n, (* nth pattern *)
 			 mkApp (Lazy.force eq_ind,
-				[| lift (lens + liftsign) ppat_ty ; liftn liftsign (succ lens) ppat_c ; 
-				   mkRel (len' + patargs.(pred n)) |]) :: 
+				[| lift (lens + liftsign) ppat_ty ;
+				   liftn liftsign (succ lens) ppat_c ; 
+				   lift len' curpat_c |]) :: 
 			   List.map (lift lens) c)
 		      in Some acc
 		    else None)
@@ -1750,7 +1753,7 @@ let constrs_of_pats typing_fun tycon env isevars eqns tomatchs sign neqs arity =
 	 let pattern_rels = fst (List.fold_right (fun (sign, pat_c, pat_ty, _, pat)  (l, acc) -> 
 						    acc :: l, List.length sign + acc) pats ([], 1))
 	 in
-	 let ineqs = build_ineqs prevpatterns newpatterns signlen (Array.of_list pattern_rels) in
+	 let ineqs = build_ineqs prevpatterns pats signlen in
 	 let eqs_rels = List.fold_left (fun eqenv (_,_,_,(eqs,ty), _) -> 
 					  (List.map (fun (x,y) -> (x, None, y)) eqs) @ eqenv)
 	   [] pats
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 33e7e1627..94f1bdec0 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -239,23 +239,23 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 		    mkRel 1
 		 |])
   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 _ -> ());
+  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 *\) *)
 (*       (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 = substnl [projection] after_length top_arity in (* substitute the projection of wfarg for arg *)
+  let intern_arity = substl [projection] intern_arity in (* substitute the projection of wfarg for arg *)
   (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 _ -> ()); *)
   let intern_before_env = push_rel_context before env in
-  let intern_fun_bl = liftafter @ [wfarg 1]  in (* FixMe dependencies *)
+(*   let intern_fun_bl = liftafter @ [wfarg 1]  in (\* FixMe dependencies *\) *)
 (*   (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *)
-  let intern_fun_arity = intern_arity in
-  (try trace (str "Intern fun arity: " ++
-		  my_print_constr _intern_env intern_fun_arity) with _ -> ());
-  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
+  (try trace (str "Intern arity: " ++
+		  my_print_constr _intern_env intern_arity) with _ -> ());
+  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
   (try trace (str "Intern fun arity product: " ++
 		  my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ());
   let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in