Fixes in Program well-founded definitions:

- de Bruijn bug #2083
- Avoid useless eta-expansion (bug #2060)


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

1 files changed, 15 insertions, 19 deletions

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 674805962d..04f57331d9 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -207,12 +207,12 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let wf_rel, wf_rel_fun, measure_fn = 
     let rconstr_body, rconstr = 
       let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in
-       let env = push_rel_context [arg] envwf in
-       let capp = interp_constr isevars env app in
- 	 capp, mkLambda (argname, argtyp, capp)
-     in
+      let env = push_rel_context [arg] envwf in
+      let capp = interp_constr isevars env app in
+ 	capp, mkLambda (argname, argtyp, capp)
+    in
       trace (str"rconstr_body: " ++ pr rconstr_body);
-       if measure then
+      if measure then
  	let lt_rel = constr_of_global (Lazy.force lt_ref) in
  	let name s = Name (id_of_string s) in
  	let wf_rel_fun lift x y = (* lift to before_env *)
@@ -241,10 +241,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let intern_bl = wfarg 1 :: arg :: before in
   let _intern_env = push_rel_context intern_bl env in
   let proj = (Lazy.force sig_).Coqlib.proj1 in
-  let projection = 
+  let projection = (* in wfarg :: arg :: before *)
     mkApp (proj, [| argtyp ;
 		    (mkLambda (Name argid', argtyp,
-			       (wf_rel_fun 1 (mkRel 1) (mkRel 3)))) ;
+			      (wf_rel_fun 3 (mkRel 1) (mkRel 3)))) ;
 		    mkRel 1
 		 |])
   in
@@ -257,12 +257,12 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   (* arity is now in something :: wfarg :: arg :: before 
      where what refered to arg now refers to something *)
   let intern_arity = substl [projection] intern_arity in
-  (* substitute the projection of wfarg for something *)
-  let intern_before_env = push_rel_context before env in
+  (* substitute the projection of wfarg for something, 
+     now intern_arity is in wfarg :: arg :: before *)
   let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
   let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
   let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
-  let fun_env = push_rel_context fun_bl intern_before_env in
+  let fun_env = push_rel_context fun_bl envwf in
   let fun_arity = interp_type_evars isevars fun_env arityc in
   let intern_body = interp_casted_constr isevars fun_env body fun_arity in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
@@ -277,7 +277,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   in
   let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
     (* Lift to get to constant arguments *)
-  let lift_cst = List.length after + 1 in
+(*   let lift_cst = List.length after + 1 in *)
   let fix_def =
     match measure_fn with
 	None ->
@@ -285,17 +285,13 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 		 [| argtyp ;
 		    wf_rel ;
 		    make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
-		    lift lift_cst prop ;
-		    lift lift_cst intern_body_lam |])
+		    prop ; intern_body_lam |])
       | Some f ->
 	  mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), 
-		[| lift lift_cst argtyp ; 
-		   lift lift_cst f ;
-		   lift lift_cst prop ;
-		   lift lift_cst intern_body_lam |])
+		[| argtyp ; f ; prop ; intern_body_lam |])
   in
-  let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
-  let def = it_mkLambda_or_LetIn def_appl binders_rel in
+  let def_appl = (* applist (fix_def, gen_rels (after_length + 1)) *) fix_def in
+  let def = it_mkLambda_or_LetIn def_appl before in
   let typ = it_mkProd_or_LetIn top_arity binders_rel in
   let fullcoqc = Evarutil.nf_isevar !isevars def in
   let fullctyp = Evarutil.nf_isevar !isevars typ in