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

1 files changed, 8 insertions, 8 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 33e7e1627d..94f1bdec0a 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