Mise en place d'une nouvelle strategie plus efficace pour les preuves de Function.

=> Changement d'ordre et de forme des obligations de preuve generees (pas de la semantique des obligations).

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

2 files changed, 171 insertions, 99 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 26708de081..32fa1903f4 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -46,10 +46,10 @@ let observe_tac_stream s tac g =
 
 let observe_tac s tac g = observe_tac_stream (str s) tac g
 
-let tclTRYD tac = 
-  if  !Options.debug  || do_observe ()
-  then (fun g -> try (* do_observe_tac ""  *)tac g with _ -> tclIDTAC g)
-  else tac
+(* let tclTRYD tac =  *)
+(*   if  !Options.debug  || do_observe () *)
+(*   then (fun g -> try (\* do_observe_tac ""  *\)tac g with _ -> tclIDTAC g) *)
+(*   else tac *)
 
 
 let list_chop ?(msg="") n l = 
@@ -136,11 +136,11 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
   fun g -> 
     let prov_id = pf_get_new_id hyp_id g in 
     tclTHENS
-      (observe_tac msg (forward (Some  (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t))
+      ((* observe_tac msg *) (forward (Some  (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t))
       [tclTHENLIST 
       [	
-	observe_tac "change_hyp_with_using thin" (thin [hyp_id]);
-	observe_tac "change_hyp_with_using rename " (h_rename prov_id hyp_id)
+	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
+	(* observe_tac "change_hyp_with_using rename " *) (h_rename prov_id hyp_id)
       ]] g
 
 exception TOREMOVE
@@ -179,7 +179,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
 let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  = 
   let nochange msg  = 
     begin 
-      observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t    );
+(*       observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t    ); *)
       failwith "NoChange"; 
     end
   in    
@@ -195,7 +195,7 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type  =
     in 
     if not (closed0 t1) then nochange "not a closed lhs";    
     let rec compute_substitution sub t1 t2 = 
-      observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2);
+(*       observe (str "compute_substitution : " ++ pr_lconstr t1 ++ str " === " ++ pr_lconstr t2); *)
       if isRel t2 
       then 
 	let t2 = destRel t2  in 
@@ -386,11 +386,12 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 			       List.rev_map mkVar (rec_pte_id::context_hyps_ids)
 			      )
 		     in
-		     observe_tac "rec hyp "
+(* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
 		       (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x)
-		       [observe_tac "prove rec hyp" (prove_rec_hyp eq_hyps);
-			observe_tac "prove rec hyp"
+		       [
+			 (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
+(* 			observe_tac "prove rec hyp" *)
 			  (refine to_refine)
 		       ])
 		       g
@@ -399,7 +400,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	    in
 	    tclTHENLIST 
 	      [
-		observe_tac "hyp rec" 
+(* 		observe_tac "hyp rec"  *)
 		  (change_hyp_with_using "rec_hyp_tac" hyp_id real_type_of_hyp prove_new_type_of_hyp);
 		scan_type context popped_t'
 	      ]
@@ -440,7 +441,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	  in
 	  tclTHENLIST[
 	    change_hyp_with_using "prove_trivial" hyp_id real_type_of_hyp 
-	      (observe_tac "prove_trivial" prove_trivial);
+	      ((* observe_tac "prove_trivial" *) prove_trivial);
 	    scan_type context popped_t'
 	  ]
 	else if is_trivial_eq t_x 
@@ -456,7 +457,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		"prove_trivial_eq"
 		hyp_id
 		real_type_of_hyp
-		(observe_tac "prove_trivial_eq" (prove_trivial_eq hyp_id context (args.(0),args.(1))));
+		((* observe_tac "prove_trivial_eq" *) (prove_trivial_eq hyp_id context (args.(0),args.(1))));
 	      scan_type context popped_t'
 	    ] 
 	else 
@@ -505,7 +506,7 @@ let clean_goal_with_heq ptes_infos continue_tac dyn_infos  =
     tclTHENLIST 
       [
 	tac ;
-	observe_tac "clean_hyp_with_heq continue" (continue_tac new_infos)
+	(* observe_tac "clean_hyp_with_heq continue" *) (continue_tac new_infos)
       ]
       g    
 
@@ -523,7 +524,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	introduction_no_check heq_id;
 	(* Then the new hypothesis *) 
 	tclMAP introduction_no_check dyn_infos.rec_hyps;
-	observe_tac "after_introduction" (fun g' -> 
+	(* observe_tac "after_introduction"  *)(fun g' -> 
 	   (* We get infos on the equations introduced*)
 	   let new_term_value_eq = pf_type_of g' (mkVar heq_id) in 
 	   (* compute the new value of the body *)
@@ -637,7 +638,7 @@ let build_proof
 		  (fun g' -> 
 		     let g'_nb_prod = nb_prod (pf_concl g') in 
 		     let nb_instanciate_partial = g'_nb_prod - g_nb_prod in 
-		     observe_tac "treat_new_case" 
+(* 		     observe_tac "treat_new_case"  *)
 		       (treat_new_case  
 		       ptes_infos
 		       nb_instanciate_partial 
@@ -668,7 +669,7 @@ let build_proof
 				  nb_rec_hyps  = List.length new_hyps
 			       }
 			   in 
-			   observe_tac "Lambda" (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
+(* 			   observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
 			     (* 			   build_proof do_finalize new_infos g' *)
 			) g
 		  | _ ->
@@ -777,14 +778,14 @@ let build_proof
 		{dyn_infos with info = arg }
 		g
       in
-      observe_tac "build_proof_args" (tac ) g
+      (* observe_tac "build_proof_args" *) (tac ) g
    in
    let do_finish_proof dyn_infos = 
      (* tclTRYD *) (clean_goal_with_heq 
       ptes_infos
       finish_proof dyn_infos)
   in
-  observe_tac "build_proof"
+  (* observe_tac "build_proof" *)
     (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos) 
 
 
@@ -857,8 +858,8 @@ let generalize_non_dep hyp g =
   in
 (*   observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
   tclTHEN 
-    (observe_tac "h_generalize" (h_generalize  (List.map mkVar to_revert) ))
-    (observe_tac "thin" (thin to_revert))
+    ((* observe_tac "h_generalize" *) (h_generalize  (List.map mkVar to_revert) ))
+    ((* observe_tac "thin" *) (thin to_revert))
     g
   
 let id_of_decl (na,_,_) =  (Nameops.out_name na)
@@ -899,11 +900,11 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     tclTHENSEQ
       [
 	tclDO (nb_params + rec_args_num + 1) intro;
-	observe_tac "" (fun g ->
+	(* observe_tac "" *) (fun g ->
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
-	     [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
-	      observe_tac "h_case" (h_case(mkVar rec_id,Rawterm.NoBindings));
+	     [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
+	      (* observe_tac "h_case" *) (h_case(mkVar rec_id,Rawterm.NoBindings));
 	      intros_reflexivity] g
 	)
       ]
@@ -1132,7 +1133,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    in 
 	    if other_fix_infos = [] 
 	    then
-	      observe_tac ("h_fix") (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
+	      (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
 	    else
 	      h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
 		other_fix_infos
@@ -1140,10 +1141,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
     in
     let first_tac : tactic = (* every operations until fix creations *)
       tclTHENSEQ 
-	[ observe_tac "introducing params" (intros_using (List.rev_map id_of_decl princ_info.params)); 
-	  observe_tac "introducing predictes" (intros_using (List.rev_map id_of_decl princ_info.predicates)); 
-	  observe_tac "introducing branches" (intros_using (List.rev_map id_of_decl princ_info.branches)); 
-	  observe_tac "building fixes" mk_fixes;
+	[ (* observe_tac "introducing params" *) (intros_using (List.rev_map id_of_decl princ_info.params)); 
+	  (* observe_tac "introducing predictes" *) (intros_using (List.rev_map id_of_decl princ_info.predicates)); 
+	  (* observe_tac "introducing branches" *) (intros_using (List.rev_map id_of_decl princ_info.branches)); 
+	  (* observe_tac "building fixes" *) mk_fixes;
 	]
     in
     let intros_after_fixes : tactic = 
@@ -1156,7 +1157,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	  let nb_args = fix_info.nb_realargs in 
 	  tclTHENSEQ
 	    [
-	      observe_tac ("introducing args") (tclDO nb_args intro);
+	      (* observe_tac ("introducing args") *) (tclDO nb_args intro);
 	      (fun g -> (* replacement of the function by its body *)
 		 let args = nLastHyps nb_args g in 
 		 let fix_body = fix_info.body_with_param in
@@ -1174,7 +1175,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		 in
 		 tclTHENSEQ
 		   [
-		     observe_tac "do_replace" 
+(* 		     observe_tac "do_replace"  *)
 		       (do_replace 
 			  full_params 
 			  (fix_info.idx + List.length princ_params) 
@@ -1199,7 +1200,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 			    nb_rec_hyps = List.length branches
 			 }
 		       in
-		       observe_tac "cleaning" (clean_goal_with_heq
+		       (* observe_tac "cleaning" *) (clean_goal_with_heq
 			 (Idmap.map prove_rec_hyp ptes_to_fix) 
 			 do_prove 
 			 dyn_infos)
@@ -1209,7 +1210,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 (* 			   str "args := " ++ prlist_with_sep spc Ppconstr.pr_id  args_id *)
 			   
 (* 			   ); *)
-		     observe_tac "instancing" (instanciate_hyps_with_args prove_tac 
+		     (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac 
 		       (List.rev_map id_of_decl princ_info.branches) 
 		       (List.rev args_id))
 		   ]
@@ -1289,18 +1290,28 @@ and h_intros = Recdef.h_intros
 and list_rewrite = Recdef.list_rewrite
 and evaluable_of_global_reference = Recdef.evaluable_of_global_reference
 
+
+
+
+
 let prove_with_tcc tcc_lemma_constr eqs : tactic =
   match !tcc_lemma_constr with
     | None -> anomaly "No tcc proof !!"
     | Some lemma ->
 	fun gls ->
 	  let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+(* 	  let ids = hid::pf_ids_of_hyps gls in  *)
 	  tclTHENSEQ
 	    [
 	      generalize [lemma];
 	      h_intro hid;
 	      Elim.h_decompose_and (mkVar hid);
 	      tclTRY(list_rewrite true eqs);
+(* 	      (fun g ->  *)
+(* 		 let ids' = pf_ids_of_hyps g in  *)
+(* 		 let ids = List.filter (fun id -> not (List.mem id ids)) ids' in  *)
+(* 		 rewrite *)
+(* 	      ) *)
 	      Eauto.gen_eauto false (false,5) [] (Some [])
 	    ]
 	    gls
@@ -1326,7 +1337,24 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
 
     
     
-  
+let build_clause eqs = 
+  {
+    Tacexpr.onhyps = 
+      Some (List.map 
+	      (fun id -> ([],id),Tacexpr.InHyp)
+	      eqs
+	   );
+    onconcl = false; 
+    concl_occs = [] 
+  }
+
+let rec rewrite_eqs_in_eqs eqs = 
+  match eqs with 
+    | [] -> tclIDTAC
+    | eq::eqs -> 
+	  tclTHEN 
+	    (tclMAP (fun id -> tclTRY (Equality.general_rewrite_in true id (mkVar eq))) eqs)
+	    (rewrite_eqs_in_eqs eqs) 
 
 let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic = 
    match !tcc_lemma_constr with 
@@ -1337,7 +1365,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
 	    (tclTHENSEQ 
 	    [
 	      backtrack_eqs_until_hrec hrec eqs;
-	      observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" )
+	      (* observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) *)
 		(tclTHENS  (* We must have exactly ONE subgoal !*)
 		   (apply (mkVar hrec))
 		   [ tclTHENSEQ 
@@ -1363,15 +1391,17 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
 			    else tclIDTAC g
 			 );
 			 observe_tac "rew_and_finish"
-			   (tclTHEN 
-			      (tclTRY(Recdef.list_rewrite true (List.map mkVar eqs)))
-			      (observe_tac "finishing"  
+			   (tclTHENLIST 
+			      [tclTRY(Recdef.list_rewrite false (List.map mkVar eqs));
+			       rewrite_eqs_in_eqs eqs;
+			       (observe_tac "finishing"  
 				 (tclCOMPLETE (
 				    Eauto.gen_eauto false (false,5) [] (Some []))
 				 )
-			      )
+			       )
+			      ]
 			   )
-		       ]
+			   ]
 		   ])
 	    ])
 	      gls
@@ -1429,14 +1459,14 @@ let prove_principle_for_gen
   in
   let real_rec_arg_num = rec_arg_num - princ_info.nparams in 
   let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in 
-  observe (
-    str "princ_type := " ++ pr_lconstr  princ_type ++ fnl () ++
-    str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++ 
+(*   observe ( *)
+(*     str "princ_type := " ++ pr_lconstr  princ_type ++ fnl () ++ *)
+(*     str "princ_info.nparams := " ++ int princ_info.nparams ++ fnl () ++  *)
       
-      str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++ 
-    str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++ 
-	     str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++
-	     str "npost_rec_arg := " ++ int npost_rec_arg );
+(*       str "princ_info.nargs := " ++ int princ_info.nargs ++ fnl () ++  *)
+(*     str "rec_arg_num := " ++ int rec_arg_num ++ fnl() ++  *)
+(* 	     str "real_rec_arg_num := " ++ int real_rec_arg_num ++ fnl () ++ *)
+(* 	     str "npost_rec_arg := " ++ int npost_rec_arg ); *)
   let (post_rec_arg,pre_rec_arg) = 
     Util.list_chop npost_rec_arg princ_info.args
   in
@@ -1445,7 +1475,7 @@ let prove_principle_for_gen
       | (Name id,_,_)::_ -> id 
       | _ -> assert false 
   in
-  observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id));
+(*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
   let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in 
   let relation = substl subst_constrs relation in 
   let input_type = substl subst_constrs rec_arg_type in 
@@ -1458,16 +1488,16 @@ let prove_principle_for_gen
   in
   let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in 
   let prove_rec_arg_acc g = 
-      (observe_tac "prove_rec_arg_acc" 
+      ((* observe_tac "prove_rec_arg_acc"  *)
 	 (tclCOMPLETE
 	    (tclTHEN
 	       (forward 
-		  (Some ((fun g -> observe_tac "prove wf" (tclCOMPLETE (wf_tac is_mes)) g)))
+		  (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))
 		  (Genarg.IntroIdentifier wf_thm_id)
 		  (mkApp (delayed_force well_founded,[|input_type;relation|])))
 	       (
-		 observe_tac 
-		   "apply wf_thm" 
+		 (* observe_tac  *)
+(* 		   "apply wf_thm"  *)
 		   (h_apply ((mkApp(mkVar wf_thm_id,
 				    [|mkVar rec_arg_id |])),Rawterm.NoBindings)
 		   )
@@ -1484,19 +1514,19 @@ let prove_principle_for_gen
 	(List.rev_map (fun (na,_,_) -> Nameops.out_name na) 
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
-      observe_tac "" (forward
+      (* observe_tac "" *) (forward
 	 (Some (prove_rec_arg_acc))
 	 (Genarg.IntroIdentifier acc_rec_arg_id)
  	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
       );
-      observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids)));
+(*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++  *)
 (* 			   str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
-      observe_tac "h_fix " (h_fix (Some fix_id) (List.length args_ids + 1)); 
+      (* observe_tac "h_fix " *) (h_fix (Some fix_id) (List.length args_ids + 1)); 
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
       Equality.rewriteLR (mkConst eq_ref);
-      observe_tac "finish" (fun gl' -> 
+      (* observe_tac "finish" *) (fun gl' -> 
 	 let body = 
 	   let _,args = destApp (pf_concl gl') in 
 	   array_last args
@@ -1524,7 +1554,7 @@ let prove_principle_for_gen
 	 let pte_info = 
 	   { proving_tac =
 	       (fun eqs -> 
-		  observe_tac "new_prove_with_tcc" 
+		  (* observe_tac "new_prove_with_tcc"  *)
 		    (new_prove_with_tcc 
 		       is_mes acc_inv fix_id tcc_lemma_ref 
 		       ((List.map 
@@ -1553,7 +1583,7 @@ let prove_principle_for_gen
 	     ptes_info
 	     (body_info rec_hyps)
 	 in
-	 observe_tac "instanciate_hyps_with_args" 
+	 (* observe_tac "instanciate_hyps_with_args"  *)
 	   (instanciate_hyps_with_args 
 	      make_proof
 	      (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches)
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 9201ba1c1c..a83d5425b4 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -273,15 +273,44 @@ let  mkCaseEq a  : tactic =
 	(* commentaire de Yves: on pourra avoir des problemes si
 	   a n'est pas bien type dans l'environnement du but *)
        let type_of_a = pf_type_of g a in
-       (tclTHEN (generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])])
+       (tclTHEN (h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])])
 	  (tclTHEN 
 	     (fun g2 ->
 		change_in_concl None 
-		  (pattern_occs [([2], a)] (pf_env g2) Evd.empty (pf_concl g2))
+		  (pattern_occs [([-1], a)] (pf_env g2) Evd.empty (pf_concl g2))
 		  g2)
 	     (simplest_case a))) g);;
 
-let rec  mk_intros_and_continue (extra_eqn:bool)
+let  mkDestructEq not_on_hyp expr g =
+	let hyps = pf_hyps g in 
+(* 	let rec is_expr_context b c =  *)
+(* 	  if c = expr  *)
+(* 	  then true  *)
+(* 	  else fold_constr is_expr_context b c  *)
+(* 	in *)
+	let to_revert = 
+	  Util.map_succeed 
+	    (fun (id,_,t) -> 
+	       if List.mem id not_on_hyp || not (Termops.occur_term expr t)   then failwith "is_expr_context";
+	       id 
+	    )
+	    hyps
+	in
+	let to_revert_constr = List.rev_map mkVar to_revert in 
+	  
+	(* commentaire de Yves: on pourra avoir des problemes si
+	   a n'est pas bien type dans l'environnement du but *)
+       let type_of_a = pf_type_of g expr in
+       (tclTHEN (h_generalize (mkApp(delayed_force refl_equal, [| type_of_a; expr|])::to_revert_constr))
+	  (tclTHEN 
+	     (fun g2 ->
+		change_in_concl None 
+		  (pattern_occs [([-1], expr)] (pf_env g2) Evd.empty (pf_concl g2))
+		  g2)
+	     (simplest_case expr))), to_revert
+
+
+let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
     cont_function (eqs:constr list) (expr:constr) g =
   match kind_of_term expr with
     | Lambda (n, _, b) -> 
@@ -292,13 +321,16 @@ let rec  mk_intros_and_continue (extra_eqn:bool)
 	in
      	let new_n = pf_get_new_id n1 g in
 	  tclTHEN (h_intro new_n)
-	    (mk_intros_and_continue extra_eqn cont_function eqs 
+	    (mk_intros_and_continue thin_intros extra_eqn cont_function eqs 
 	       (subst1 (mkVar new_n) b)) g
     | _ -> 
  	if extra_eqn then
 	  let teq = pf_get_new_id teq_id g in
 	    tclTHENLIST
 	      [ h_intro teq;
+		thin thin_intros;
+		h_intros thin_intros;
+		
 		tclMAP 
 		  (fun eq -> tclTRY (Equality.general_rewrite_in true teq eq)) 
 		  (List.rev eqs);
@@ -313,7 +345,11 @@ let rec  mk_intros_and_continue (extra_eqn:bool)
 	      ]
 	      g
 	else
-	  cont_function eqs expr g
+	  tclTHENSEQ[
+	    thin thin_intros;
+	    h_intros thin_intros;
+	    cont_function eqs expr 
+	  ] g
 
 let const_of_ref = function
     ConstRef kn -> kn
@@ -321,9 +357,10 @@ let const_of_ref = function
 
 let simpl_iter () =
   reduce 
-    (Lazy 
+    (Lazy
        {rBeta=true;rIota=true;rZeta= true; rDelta=false;
         rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]})
+(*     (Simpl (Some ([],mkConst (const_of_ref (delayed_force iter_ref))))) *)
     onConcl
 
 (* The boolean value is_mes expresses that the termination is expressed
@@ -533,12 +570,15 @@ let rec introduce_all_values is_mes acc_inv func context_fn
 	      hrec args
 	      (rec_res::values)(hspec::specs)) in
 	(tclTHENS
-	   (observe_tac "elim h_rec" (simplest_elim (mkApp(mkVar hrec, Array.of_list arg))))
+	   (observe_tac "elim h_rec" 
+	      (simplest_elim (mkApp(mkVar hrec, Array.of_list arg)))
+	   )
 	   [tclTHENLIST [h_intros [rec_res; hspec];
 			 tac]; 
 	    (tclTHENS
 		 (observe_tac "acc_inv" (apply (Lazy.force acc_inv)))
-		 [ observe_tac "h_assumption" h_assumption
+		 [(* tclTHEN (tclTRY(list_rewrite true eqs)) *)
+		    (observe_tac "h_assumption" h_assumption)
 		 ;
 		  tclTHENLIST
 		    [
@@ -564,7 +604,7 @@ let rec_leaf_terminate is_mes acc_inv hrec (func:global_reference) eqs expr =
       observe_tac "introduce_all_values" 
 	(introduce_all_values is_mes acc_inv func context_fn eqs  hrec args  [] [])
 
-let proveterminate is_mes acc_inv (hrec:identifier)  
+let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)  
   (f_constr:constr) (func:global_reference) base_leaf rec_leaf = 
   let rec proveterminate (eqs:constr list) (expr:constr)  =
     try
@@ -574,17 +614,13 @@ let proveterminate is_mes acc_inv (hrec:identifier)
 	    Case (_, t, a, l) -> 
 	      (match find_call_occs f_constr a with
 		   _,[] ->
-      		     tclTHENS 
-		       (fun g ->
-			  (* let _ = msgnl(str "entering mkCaseEq") in *)
-			  let v = (mkCaseEq a) g in 
-			  (* let _ = msgnl (str "exiting mkCaseEq") in *)
-			  v
-		       )
-   	               (List.map 
-			  (mk_intros_and_continue true proveterminate eqs)
-			  (Array.to_list l)
-		       )
+		     (fun g -> 
+			let destruct_tac,rev_to_thin_intro = mkDestructEq rec_arg_id a g in 
+			tclTHENS destruct_tac
+			  (List.map 
+			     (mk_intros_and_continue (List.rev rev_to_thin_intro) true proveterminate eqs)
+			     (Array.to_list l) 
+			  ) g)
 		 | _, _::_ -> 
 		     (
 		       match find_call_occs  f_constr expr with
@@ -719,13 +755,13 @@ let termination_proof_header is_mes input_type ids args_id relation
 	       [observe_tac "generalize" 
 		  (onNLastHyps (nargs+1)
 		     (fun (id,_,_) -> 
-			tclTHEN (generalize [mkVar id]) (h_clear false [id])
+			tclTHEN (h_generalize [mkVar id]) (h_clear false [id])
 		     ))
 	       ;
 		observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
 		h_intros args_id;
 		h_intro wf_rec_arg;
-		observe_tac "tac" (tac hrec acc_inv)
+		observe_tac "tac" (tac wf_rec_arg hrec acc_inv)
 	       ]
 	   ]
 	) g  
@@ -776,8 +812,9 @@ let whole_start is_mes func input_type relation rec_arg_num  : tactic =
 	relation 
 	rec_arg_num
 	rec_arg_id
-	(fun hrec acc_inv g ->  
+	(fun rec_arg_id hrec acc_inv g ->  
            (proveterminate 
+	      [rec_arg_id]
 	      is_mes
 	      acc_inv 
 	      hrec
@@ -854,7 +891,7 @@ let prove_with_tcc lemma _ : tactic =
     let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in 
     tclTHENSEQ 
       [
-	generalize [lemma];
+	h_generalize [lemma];
 	h_intro hid;
 	Elim.h_decompose_and (mkVar hid); 
 	gen_eauto(* default_eauto *) false (false,5) [] (Some [])
@@ -1049,7 +1086,7 @@ let base_leaf_eq func eqs f_id g =
 		  [|mkApp (delayed_force coq_S, [|mkVar p|]);
 		    mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|])));
       simpl_iter();
-      unfold_in_concl [([1], evaluable_of_global_reference func)];
+      tclTRY (unfold_in_concl [([1], evaluable_of_global_reference func)]);
       list_rewrite true eqs;
       apply (delayed_force refl_equal)] g;;
 
@@ -1111,7 +1148,7 @@ let rec introduce_all_values_eq  cont_tac functional termine
 		tclTHENLIST
 		  [cont_tac pmax' le_proofs';
 		   h_intros [heq;heq2];
-		   rewriteLR (mkVar heq2);
+		   observe_tac "rewriteRL" (tclTRY (rewriteLR (mkVar heq2)));
 		   tclTHENS
 		     ( fun g -> 
 			 let t_eq = compute_renamed_type g (mkVar heq) in 
@@ -1121,12 +1158,12 @@ let rec introduce_all_values_eq  cont_tac functional termine
 			   let def_na,_,_ = destProd t in 
 			   Nameops.out_name k_na,Nameops.out_name def_na
 			 in
-			 general_rewrite_bindings false
+			 observe_tac "general_rewrite_bindings" (general_rewrite_bindings false
 			   (mkVar heq,
 			    ExplicitBindings
 			      [dummy_loc, NamedHyp k_id,
 			       f_S(mkVar pmax');
-			       dummy_loc, NamedHyp def_id, f]) 
+			       dummy_loc, NamedHyp def_id, f]) )
 			   g
 		     )
 		     [tclIDTAC;
@@ -1153,26 +1190,30 @@ let rec_leaf_eq termine f ids functional eqs expr fn args =
       [h_intros [v;hex];
        simplest_elim (mkVar hex);
        h_intros [p;heq1];
-       generalize [mkApp(delayed_force le_n,[|mkVar p|])];
+       h_generalize [mkApp(delayed_force le_n,[|mkVar p|])];
        h_intros [hle1];
-       introduce_all_values_eq
+       observe_tac "introduce_all_values_eq" (introduce_all_values_eq
 	 (fun _ _ -> tclIDTAC)
-	 functional termine f p heq1 p [] [] eqs ids args;
+	 functional termine f p heq1 p [] [] eqs ids args);
        apply (delayed_force refl_equal)]
 
 let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
     (eqs:constr list)
   (expr:constr) =
-  tclTRY
-    (match kind_of_term expr with
+(*   tclTRY *)
+  (match kind_of_term expr with
       Case(_,t,a,l) ->
 	(match find_call_occs f a with
 	     _,[] -> 
-	       tclTHENS(mkCaseEq a)(* (simplest_case a) *)
-	  	 (List.map
-		    (fun expr -> observe_tac "mk_intros_and_continue" (mk_intros_and_continue true
-		       (prove_eq  termine f functional) eqs expr))
-		    (Array.to_list l))
+	       (fun g -> 
+		  let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in 
+		  tclTHENS destruct_tac
+		    (List.map 
+		       (mk_intros_and_continue (List.rev rev_to_thin_intro) true 
+			  (prove_eq termine f functional)  
+			  eqs)
+		       (Array.to_list l) 
+		    ) g)
 	   | _,_::_ ->
                	(match find_call_occs f expr with
 	     _,[] -> base_leaf_eq functional eqs f
@@ -1211,7 +1252,7 @@ let (com_eqn : identifier ->
        (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
      by
        (start_equation f_ref terminate_ref
-	  (fun x ->
+	  (fun  x ->
 	     prove_eq 
 	       (constr_of_reference terminate_ref)
 	       f_constr 
@@ -1226,6 +1267,7 @@ let (com_eqn : identifier ->
 (*      (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
      Options.silently (fun () ->Command.save_named opacity) () ;  
+(*      Pp.msgnl (str "eqn finished"); *)
     
     );;