correction bug d'efficacite dans Function

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

2 files changed, 79 insertions, 44 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index ba17a23eea..d7c627248f 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1305,13 +1305,13 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
     | 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 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);
+(* 	      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  *)
@@ -1367,7 +1367,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
     | None -> tclIDTAC_MESSAGE (str "No tcc proof !!")
     | Some lemma -> 
 	fun gls ->
-	  let tcc_hyp = next_global_ident_away true (Names.id_of_string "tcc_p") (pf_ids_of_hyps gls) in 
+(* 	  let tcc_hyp = next_global_ident_away true (Names.id_of_string "tcc_p") (pf_ids_of_hyps gls) in  *)
 	    (tclTHENSEQ 
 	    [
 	      backtrack_eqs_until_hrec hrec eqs;
@@ -1376,18 +1376,18 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic =
 		   (apply (mkVar hrec))
 		   [ tclTHENSEQ 
 		       [
-			 generalize [lemma];
-			 h_intro tcc_hyp;
-			 begin 
-			   let eqs' : identifier list = 
-			     let sec_vars = 
-			       List.filter Termops.is_section_variable (pf_ids_of_hyps gls) 
-			     in
-			     sec_vars@eqs
-			   in
-			   keep (tcc_hyp::eqs')
-			 end;
-			 Elim.h_decompose_and (mkVar tcc_hyp); 
+(* 			 generalize [lemma]; *)
+(* 			 h_intro tcc_hyp; *)
+(* 			 begin  *)
+(* 			   let eqs' : identifier list =  *)
+(* 			     let sec_vars =  *)
+(* 			       List.filter Termops.is_section_variable (pf_ids_of_hyps gls)  *)
+(* 			     in *)
+(* 			     sec_vars@eqs *)
+(* 			   in *)
+(* 			   keep (tcc_hyp::eqs') *)
+(* 			 end; *)
+(* 			 Elim.h_decompose_and (mkVar tcc_hyp);  *)
 			 
 			 apply (Lazy.force acc_inv);
 			 (fun g -> 
@@ -1460,7 +1460,7 @@ let prove_principle_for_gen
   let wf_tac = 
     if is_mes 
     then 
-      (fun b -> Recdef.tclUSER_if_not_mes b None)
+      (fun b -> Recdef.tclUSER_if_not_mes tclIDTAC b None)
     else fun _ -> prove_with_tcc tcc_lemma_ref []
   in
   let real_rec_arg_num = rec_arg_num - princ_info.nparams in 
@@ -1512,8 +1512,25 @@ let prove_principle_for_gen
       g
   in
   let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
+  let lemma = 
+    match !tcc_lemma_ref with 
+     | None -> anomaly ( "No tcc proof !!")
+     | Some lemma -> lemma
+  in
+
+  let start_tac gls = 
+      let hid = next_global_ident_away true (id_of_string "prov") (pf_ids_of_hyps gls) in
+      tclTHENSEQ
+	[
+	  generalize [lemma];
+	  h_intro hid;
+	  Elim.h_decompose_and (mkVar hid);
+	]
+	gls
+  in
   tclTHENSEQ
-    [ 
+    [ 	      
+      observe_tac "start_tac" start_tac;
       h_intros 
 	(List.rev_map (fun (na,_,_) -> Nameops.out_name na) 
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 31c9659b10..df2755d3db 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -388,7 +388,7 @@ let simpl_iter () =
 
 (* The boolean value is_mes expresses that the termination is expressed
   using a measure function instead of a well-founded relation. *)
-let tclUSER is_mes l g = 
+let tclUSER tac is_mes l g = 
   let clear_tac = 
     match l with 
       | None -> h_clear true []
@@ -398,8 +398,8 @@ let tclUSER is_mes l g =
     [
       clear_tac;
       if is_mes 
-      then unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))]
-      else tclIDTAC
+      then tclTHEN (unfold_in_concl [([], evaluable_of_global_reference (delayed_force ltof_ref))]) tac
+      else tac (* tclIDTAC *)
     ]
     g
     
@@ -572,7 +572,7 @@ let retrieve_acc_var g =
     (fun id -> string_match (string_of_id id);id)
     hyps 
 
-let rec introduce_all_values is_mes acc_inv func context_fn
+let rec introduce_all_values concl_tac is_mes acc_inv func context_fn
     eqs  hrec args values specs =
     (match args with
     [] -> 
@@ -589,7 +589,7 @@ let rec introduce_all_values is_mes acc_inv func context_fn
 	let hspec = next_global_ident_away true hspec_id ids in
 	let tac =  
 	  observe_tac "introduce_all_values" (
-	    introduce_all_values is_mes acc_inv func context_fn eqs
+	    introduce_all_values concl_tac is_mes acc_inv func context_fn eqs
 	      hrec args
 	      (rec_res::values)(hspec::specs)) in
 	(tclTHENS
@@ -609,6 +609,7 @@ let rec introduce_all_values is_mes acc_inv func context_fn
 		      observe_tac "user proof" 
 			(fun g ->  
 			   tclUSER
+			     concl_tac
 			     is_mes
 			     (Some (hrec::hspec::(retrieve_acc_var g)@specs))
 			     g
@@ -621,11 +622,11 @@ let rec introduce_all_values is_mes acc_inv func context_fn
     )
  
 	   
-let rec_leaf_terminate is_mes acc_inv hrec (func:global_reference) eqs expr =
+let rec_leaf_terminate concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr =
   match find_call_occs 0 (mkVar (get_f (constr_of_reference func))) expr with
   | context_fn, args ->
       observe_tac "introduce_all_values" 
-	(introduce_all_values is_mes acc_inv func context_fn eqs  hrec args  [] [])
+	(introduce_all_values concl_tac is_mes acc_inv func context_fn eqs  hrec args  [] [])
 (*
 let proveterminate rec_arg_id is_mes acc_inv (hrec:identifier)  
   (f_constr:constr) (func:global_reference) base_leaf rec_leaf = 
@@ -766,10 +767,10 @@ let hyp_terminates nb_args func =
 	     
 
 
-let tclUSER_if_not_mes is_mes names_to_suppress = 
+let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = 
   if is_mes 
   then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof))
-  else tclUSER is_mes names_to_suppress
+  else tclUSER concl_tac is_mes names_to_suppress
 
 let termination_proof_header is_mes input_type ids args_id relation
     rec_arg_num rec_arg_id tac wf_tac : tactic = 
@@ -860,7 +861,7 @@ let rec instantiate_lambda t l =
 ;;
 
 
-let whole_start nb_args is_mes func input_type relation rec_arg_num  : tactic = 
+let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num  : tactic = 
   begin 
     fun g -> 
       let ids = ids_of_named_context (pf_hyps g) in
@@ -903,13 +904,13 @@ let whole_start nb_args is_mes func input_type relation rec_arg_num  : tactic =
 	      (mkVar f_id)
 	      func
 	      base_leaf_terminate 
-	      rec_leaf_terminate
+	      (rec_leaf_terminate concl_tac)
 	      []
 	      expr
 	   )
 	     g 
 	)
-	tclUSER_if_not_mes 
+	(tclUSER_if_not_mes concl_tac)
 	g 
   end
 
@@ -980,10 +981,11 @@ let prove_with_tcc lemma _ : tactic =
 	  (* 	      default_auto *)
       ]
       gls
+
       
 	     
 
-let open_new_goal using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal)   = 
+let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal)   = 
   let current_proof_name = get_current_proof_name () in
   let name = match goal_name with 
     | Some s -> s 
@@ -1008,12 +1010,23 @@ let open_new_goal using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal
 	| _ -> anomaly "equation_lemma: not a constant"
     in
     let lemma = mkConst (Lib.make_con na) in 
-    Array.iteri 
-      (fun i _ -> 
-	 by (observe_tac ("reusing lemma "^(string_of_id na)) (prove_with_tcc lemma i)))
-      (Array.make nb_goal ())
-    ;
+(*     Array.iteri  *)
+(*       (fun i _ ->  *)
+(* 	 by (observe_tac ("reusing lemma "^(string_of_id na)) (prove_with_tcc lemma (nb_goal - i)))) *)
+(*       (Array.make nb_goal ()) *)
+(*     ; *)
     ref := Some lemma ;
+    Options.silently (Vernacentries.interp (Vernacexpr.VernacAbort None));
+    build_proof 
+      (  fun gls ->
+	   let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in 
+	   tclTHENSEQ 
+	     [
+	       h_generalize [lemma];
+	       h_intro hid;
+	       Elim.h_decompose_and (mkVar hid); 
+	     ] gls)
+      (gen_eauto(* default_eauto *) false (false,5) [] (Some []));
     Command.save_named opacity;
   in
   start_proof
@@ -1046,6 +1059,8 @@ let open_new_goal using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal
     defined ()
   
 ;;    
+
+
 let com_terminate 
     tcc_lemma_name 
     tcc_lemma_ref 
@@ -1057,17 +1072,20 @@ let com_terminate
     thm_name using_lemmas 
     nb_args
     hook =
-  let (evmap, env) = Command.get_current_context() in
-  start_proof thm_name
-    (Global, Proof Lemma) (Environ.named_context_val env)
-    (hyp_terminates nb_args fonctional_ref) hook;
-  by (observe_tac "whole_start" (whole_start nb_args is_mes fonctional_ref
+  let start_proof (tac_start:tactic) (tac_end:tactic) = 
+    let (evmap, env) = Command.get_current_context() in
+    start_proof thm_name
+      (Global, Proof Lemma) (Environ.named_context_val env)
+      (hyp_terminates nb_args fonctional_ref) hook;
+    by (observe_tac "starting_tac" tac_start);
+    by (observe_tac "whole_start" (whole_start tac_end nb_args is_mes fonctional_ref
 				   input_type relation rec_arg_num ))
     
-  ;
+  in
+  start_proof tclIDTAC tclIDTAC;
   try 
     let new_goal_type = build_new_goal_type () in 
-    open_new_goal using_lemmas tcc_lemma_ref
+    open_new_goal start_proof using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
       (new_goal_type)
   with Failure "empty list of subgoals!" ->