Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.

Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).


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

6 files changed, 20 insertions, 22 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 32fa1903f4..bd4cd0d8c9 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1353,7 +1353,7 @@ let rec rewrite_eqs_in_eqs eqs =
     | [] -> tclIDTAC
     | eq::eqs -> 
 	  tclTHEN 
-	    (tclMAP (fun id -> tclTRY (Equality.general_rewrite_in true id (mkVar eq))) eqs)
+	    (tclMAP (fun id -> tclTRY (Equality.general_rewrite_in true id (mkVar eq) false)) eqs)
 	    (rewrite_eqs_in_eqs eqs) 
 
 let new_prove_with_tcc is_mes acc_inv hrec tcc_lemma_constr eqs : tactic = 
@@ -1498,9 +1498,7 @@ let prove_principle_for_gen
 	       (
 		 (* observe_tac  *)
 (* 		   "apply wf_thm"  *)
-		   (h_apply ((mkApp(mkVar wf_thm_id,
-				    [|mkVar rec_arg_id |])),Rawterm.NoBindings)
-		   )
+		 h_simplest_apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))
 	       )
 	    )
 	 )
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index d6dcccba61..b78aa98453 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -151,7 +151,7 @@ let pp_string x =
 let unify_e_resolve  (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false clenv' gls in
-    simplest_eapply c gls
+    Hiddentac.h_simplest_eapply c gls
 
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl = 
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index b1809523c4..d96b639531 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function
   | PbpRight -> TacAtom (zz, TacRight NoBindings)
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
-  | PbpApply h -> TacAtom (zz, TacApply (make_var h,NoBindings))
+  | PbpApply h -> TacAtom (zz, TacApply (false,(make_var h,NoBindings)))
   | PbpElim (hyp_name, names) ->
       let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
       TacAtom
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 4bec73501f..48c9b9eb4a 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1202,7 +1202,7 @@ let rec natural_ntree ig ntree =
 	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
               natural_induction ig lh g gs ge id ltree true
-	  | TacApply (c,_) -> natural_apply ig lh g gs c ltree
+	  | TacApply (false,(c,_)) -> natural_apply ig lh g gs c ltree
 	  | TacExact c -> natural_exact ig lh g gs c ltree
 	  | TacCut c -> natural_cut ig lh g gs c ltree
 	  | TacExtend (_,"CutIntro",[a]) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 639b4ae747..1ac99efcb2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1004,12 +1004,13 @@ and xlate_tac =
 		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
 	in 
 	CT_replace_with (c1, c2,cl,tac_opt)
-    | TacRewrite(b,cbindl,cl) -> 
+    | TacRewrite(b,false,cbindl,cl) -> 
      let cl = xlate_clause cl 
      and c = xlate_formula (fst cbindl) 
      and bindl = xlate_bindings (snd cbindl) in
      if b then CT_rewrite_lr (c, bindl, cl)
      else CT_rewrite_rl (c, bindl, cl)
+    | TacRewrite(b,true,cbindl,cl) -> xlate_error "TODO: erewrite"
     | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
      let t = out_gen rawwit_main_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
@@ -1122,10 +1123,9 @@ and xlate_tac =
       (match out_gen rawwit_int_or_var n with
 	| ArgVar _ -> xlate_error ""
 	| ArgArg n -> CT_prolog (CT_formula_list cl, CT_int  n))
-    | TacExtend (_,"eapply", [cbindl]) ->
-     let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
-     let c = xlate_formula c and bindl = xlate_bindings bindl in
-     CT_eapply (c, bindl)
+    (* eapply now represented by TacApply (true,cbindl) 
+    | TacExtend (_,"eapply", [cbindl]) -> 
+*)
     | TacTrivial ([],Some []) -> CT_trivial
     | TacTrivial ([],None) -> 
 	CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
@@ -1136,8 +1136,10 @@ and xlate_tac =
 	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
-    | TacApply (c,bindl) ->
+    | TacApply (false,(c,bindl)) ->
      CT_apply (xlate_formula c, xlate_bindings bindl)
+    | TacApply (true,(c,bindl)) ->
+     CT_eapply (xlate_formula c, xlate_bindings bindl)
     | TacConstructor (n_or_meta, bindl) ->
 	let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
 	in CT_constructor (CT_int n, xlate_bindings bindl)
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index a83d5425b4..45f0a19752 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -332,7 +332,7 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		h_intros thin_intros;
 		
 		tclMAP 
-		  (fun eq -> tclTRY (Equality.general_rewrite_in true teq eq)) 
+		  (fun eq -> tclTRY (Equality.general_rewrite_in true teq eq false)) 
 		  (List.rev eqs);
 		(fun g1 -> 
 		   let ty_teq = pf_type_of g1 (mkVar teq) in 
@@ -476,7 +476,7 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
 	   (general_rewrite_bindings false
 	      (mkVar eq,
 	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
-				dummy_loc, NamedHyp def_id, mkVar def]))
+				dummy_loc, NamedHyp def_id, mkVar def]) false)
 	   [list_cond_rewrite k def pmax eqs le_proofs;
             observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g
       ) 
@@ -684,8 +684,7 @@ let hyp_terminates func =
 
 let tclUSER_if_not_mes is_mes names_to_suppress = 
   if is_mes 
-  then 
-    tclCOMPLETE (h_apply (delayed_force well_founded_ltof,Rawterm.NoBindings))
+  then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof))
   else tclUSER is_mes names_to_suppress
 
 let termination_proof_header is_mes input_type ids args_id relation
@@ -745,8 +744,7 @@ let termination_proof_header is_mes input_type ids args_id relation
 		 (* this gives the accessibility argument *)
 		 observe_tac 
 		   "apply wf_thm" 
-		   (h_apply ((mkApp(mkVar wf_thm,
-				    [|mkVar rec_arg_id |])),Rawterm.NoBindings)
+		   (h_simplest_apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))
 		   )
 	       ]
 	     ;
@@ -950,7 +948,7 @@ let open_new_goal using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal
 	      (fun c -> 
 		 tclTHENSEQ
 		   [intros; 
-		    h_apply (interp_constr Evd.empty (Global.env()) c,Rawterm.NoBindings); 
+		    h_simplest_apply (interp_constr Evd.empty (Global.env()) c); 
 		    tclCOMPLETE Auto.default_auto
 		   ]
 	      )
@@ -1111,7 +1109,7 @@ let rec introduce_all_values_eq  cont_tac functional termine
 		 ExplicitBindings[dummy_loc,NamedHyp k_id,
 				  f_S(f_S(mkVar pmax));
 				  dummy_loc,NamedHyp def_id,
-				  f]) gls )
+				  f]) false gls )
 	     [tclTHENLIST
 		[simpl_iter();
 		 unfold_constr (reference_of_constr functional);
@@ -1163,7 +1161,7 @@ let rec introduce_all_values_eq  cont_tac functional termine
 			    ExplicitBindings
 			      [dummy_loc, NamedHyp k_id,
 			       f_S(mkVar pmax');
-			       dummy_loc, NamedHyp def_id, f]) )
+			       dummy_loc, NamedHyp def_id, f]) false)
 			   g
 		     )
 		     [tclIDTAC;