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

25 files changed, 152 insertions, 128 deletions

diff --git a/CHANGES b/CHANGES
index 9db0cec4eb..e0353a1947 100644
--- a/CHANGES
+++ b/CHANGES
@@ -37,6 +37,7 @@ Tactics
 - Slight improvement of the hnf and simpl tactics when applied on
   expressions with explicit occurrences of match or fix.
 - Better heuristic of lemma unfolding for apply/eapply.
+- New tactics "eapply in", "erewrite", "erewrite in".
 
 Changes from V8.1gamma to V8.1
 ==============================
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;
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index ad5704db8e..ad7eaaf5e7 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -8,7 +8,8 @@ A few differences in Coq ML interfaces between Coq V8.0 and V8.1
 ** Functions
 
 Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
-
+Tactics: apply_with_bindings -> apply_with_bindings_wo_evars
+Eauto.simplest_apply -> Hiddentac.h_simplest_apply
 
 =========================================
 = CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index fe21a876cf..3cbd12e539 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -321,7 +321,8 @@ GEXTEND Gram
       | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
       | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
 
-      | IDENT "apply"; cl = constr_with_bindings -> TacApply cl
+      | IDENT "apply"; cl = constr_with_bindings -> TacApply (false,cl)
+      | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,cl)
       | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
           TacElim (cl,el)
       | IDENT "elimtype"; c = constr -> TacElimType c
@@ -422,8 +423,10 @@ GEXTEND Gram
       | IDENT "transitivity"; c = constr -> TacTransitivity c
 
       (* Equality and inversion *)
-      | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause -> 
-	  TacRewrite (b,c,cl)
+      | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause ->
+	  TacRewrite (b,false,c,cl)
+      | IDENT "erewrite"; b = orient; c = constr_with_bindings ; cl = clause ->
+	  TacRewrite (b,true,c,cl)
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
 	  | IDENT "inversion" -> FullInversion
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index a70c9acdbb..9218fb816a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -664,7 +664,9 @@ and pr_atom1 = function
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
   | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
-  | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb)
+  | TacApply (ev,cb) ->
+      hov 1 (str (if ev then "eapply" else "apply") ++ spc () ++ 
+             pr_with_bindings cb)
   | TacElim (cb,cbo) ->
       hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ 
         pr_opt pr_eliminator cbo)
@@ -805,9 +807,9 @@ and pr_atom1 = function
   | TacTransitivity c -> str "transitivity" ++ pr_constrarg c
 
   (* Equality and inversion *)
-  | TacRewrite (b,c,cl) -> 
-      hov 1 (str "rewrite" ++ pr_orient b ++ spc() ++ pr_with_bindings c ++ 
-             pr_clauses pr_ident cl) 
+  | TacRewrite (b,ev,c,cl) -> 
+      hov 1 (str (if ev then "erewrite" else "rewrite") ++ pr_orient b ++
+             spc() ++ pr_with_bindings c ++ pr_clauses pr_ident cl) 
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index bea93a39c3..ef25e9b8d6 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -273,8 +273,8 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
   | Tacexpr.TacVmCastNoCheck c ->
       <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
-  | Tacexpr.TacApply cb ->
-      <:expr< Tacexpr.TacApply $mlexpr_of_constr_with_binding cb$ >>
+  | Tacexpr.TacApply (false,cb) ->
+      <:expr< Tacexpr.TacApply False $mlexpr_of_constr_with_binding cb$ >>
   | Tacexpr.TacElim (cb,cbo) ->
       let cb = mlexpr_of_constr_with_binding cb in
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index b855ee7e0a..944d7d4b39 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -81,6 +81,8 @@ val clenv_unique_resolver :
 val evar_clenv_unique_resolver :
   clausenv -> evar_info sigma -> clausenv
 
+val clenv_pose_dependent_evars : clausenv -> clausenv
+
 (***************************************************************)
 (* Bindings *)
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 633a9a42d3..14794086ab 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -21,6 +21,7 @@ type 'a or_metaid = AI of 'a | MetaId of loc * string
 
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag = bool      (* true = lazy             false = eager *)
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 
 type raw_red_flag =
   | FBeta
@@ -122,7 +123,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacExact of 'constr
   | TacExactNoCheck of 'constr
   | TacVmCastNoCheck of 'constr
-  | TacApply of 'constr with_bindings
+  | TacApply of evars_flag * 'constr with_bindings
   | TacElim of 'constr with_bindings * 'constr with_bindings option
   | TacElimType of 'constr
   | TacCase of 'constr with_bindings
@@ -184,7 +185,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacTransitivity of 'constr 
 
   (* Equality and inversion *)
-  | TacRewrite of bool * 'constr with_bindings * 'id gclause
+  | TacRewrite of bool * evars_flag * 'constr with_bindings * 'id gclause
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
       
   (* For ML extensions *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 06178324d9..2049eb0f6a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -235,7 +235,7 @@ let thin l             = with_check (thin_no_check l)
 let thin_body c        = with_check (thin_body_no_check c)
 let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
 let rename_hyp id id'  = with_check (rename_hyp_no_check id id')
-    
+
 (* Pretty-printers *)
 
 open Pp
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index eb8e07173d..e2ce6baeb3 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -82,7 +82,7 @@ let autorewrite tac_main lbas =
     (List.fold_left (fun tac bas -> 
        tclTHEN tac (one_base general_rewrite tac_main bas)) tclIDTAC lbas))
 
-let autorewrite_mutlti_in idl tac_main lbas : tactic =
+let autorewrite_multi_in idl tac_main lbas : tactic =
   fun gl -> 
  (* let's check at once if id exists (to raise the appropriate error) *)
  let _ = List.map (Tacmach.pf_get_hyp gl) idl in
@@ -96,7 +96,7 @@ let autorewrite_mutlti_in idl tac_main lbas : tactic =
       | _ -> (* even the hypothesis id is missing *)
              error ("No such hypothesis : " ^ (string_of_id !id))
     in
-    let gl' = general_rewrite_in dir !id cstr gl in
+    let gl' = general_rewrite_in dir !id cstr false gl in
     let gls = (fst gl').Evd.it in
     match gls with
        g::_ ->
@@ -126,11 +126,11 @@ let autorewrite_mutlti_in idl tac_main lbas : tactic =
        tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) tclIDTAC lbas)))
    idl gl
 
-let autorewrite_in id = autorewrite_mutlti_in [id]
+let autorewrite_in id = autorewrite_multi_in [id]
 
 let gen_auto_multi_rewrite tac_main lbas cl = 
   let try_do_hyps treat_id l = 
-    autorewrite_mutlti_in (List.map treat_id l) tac_main lbas
+    autorewrite_multi_in (List.map treat_id l) tac_main lbas
   in 
   if cl.concl_occs <> [] then 
     error "The \"at\" syntax isn't available yet for the autorewrite tactic"
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 310b70fd97..c450bf6228 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -29,6 +29,7 @@ open Pattern
 open Clenv
 open Auto
 open Rawterm
+open Hiddentac
 
 let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
   if occur_existential t1 or occur_existential t2 then 
@@ -54,13 +55,6 @@ let registered_e_assumption gl =
   tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) 
               (pf_ids_of_hyps gl)) gl
 
-(* This automatically define h_eApply (among other things) *)
-TACTIC EXTEND eapply
-  [ "eapply" constr_with_bindings(c) ] -> [ Tactics.eapply_with_bindings c ]
-END
-
-let simplest_eapply c = h_eapply (c,NoBindings)
-
 let e_constructor_tac boundopt i lbind gl = 
     let cl = pf_concl gl in 
   let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in 
@@ -130,8 +124,8 @@ END
 
 let one_step l gl =
   [Tactics.intro]
-  @ (List.map simplest_eapply (List.map mkVar (pf_ids_of_hyps gl)))
-  @ (List.map simplest_eapply l)
+  @ (List.map h_simplest_eapply (List.map mkVar (pf_ids_of_hyps gl)))
+  @ (List.map h_simplest_eapply l)
   @ (List.map assumption (pf_ids_of_hyps gl))
 
 let rec prolog l n gl =
@@ -162,7 +156,7 @@ open Auto
 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
+  h_simplest_eapply c gls
 
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl = 
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 589ac5abe9..8fac813a63 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -22,11 +22,7 @@ val e_assumption : tactic
 
 val registered_e_assumption : tactic
 
-val simplest_eapply : constr -> tactic
-
 val e_give_exact_constr : constr -> tactic
 
 val gen_eauto : bool -> bool * int -> constr list -> 
   hint_db_name list option -> tactic
-
-val simplest_eapply : constr -> tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ee950e55ff..af5545fed2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -56,14 +56,14 @@ let general_s_rewrite_clause = function
   | Some id -> general_s_rewrite_in id
 
 (* Ad hoc asymmetric general_elim_clause *)
-let general_elim_clause cls c elim = match cls with
+let general_elim_clause with_evars cls c elim = match cls with
   | None ->
       (* was tclWEAK_PROGRESS which only fails for tactics generating one 
          subgoal and did not fail for useless conditional rewritings generating
          an extra condition *)
       tclNOTSAMEGOAL (general_elim c elim ~allow_K:false)
   | Some id ->
-      general_elim_in id c elim 
+      general_elim_in with_evars id c elim 
 
 let elimination_sort_of_clause = function
   | None -> elimination_sort_of_goal
@@ -81,7 +81,7 @@ let elimination_sort_of_clause = function
    else back to the old approach
 *)
 
-let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
+let general_rewrite_bindings_clause cls lft2rgt (c,l) with_evars gl =
   let ctype = pf_apply get_type_of gl c in 
   (* A delta-reduction would be here too strong, since it would 
      break search for a defined setoid relation in head position. *)
@@ -109,17 +109,17 @@ let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
 		with Not_found ->
 		  error ("Cannot find rewrite principle "^rwr_thm)
               in 
-		general_elim_clause cls (c,l) (elim,NoBindings) gl
+		general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
 
 let general_rewrite_bindings = general_rewrite_bindings_clause None
-let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings)
+let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings) false
 
 let general_rewrite_bindings_in l2r id =
   general_rewrite_bindings_clause (Some id) l2r
 let general_rewrite_in l2r id c = 
   general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
 
-let general_multi_rewrite l2r c cl = 
+let general_multi_rewrite l2r with_evars c cl = 
   if cl.concl_occs <> [] then 
     error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
   else match cl.onhyps with 
@@ -129,10 +129,14 @@ let general_multi_rewrite l2r c cl =
 	let rec do_hyps = function 
 	  | [] -> tclIDTAC
 	  | ((_,id),_) :: l -> 
-	      tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
+	      tclTHENFIRST
+	        (general_rewrite_bindings_in l2r id c with_evars)
+	        (do_hyps l)
 	in 
-	if not cl.onconcl then do_hyps l 
-	else tclTHENFIRST (general_rewrite_bindings l2r c) (do_hyps l)
+	if not cl.onconcl then do_hyps l else
+	  tclTHENFIRST
+	    (general_rewrite_bindings l2r c with_evars)
+	    (do_hyps l)
     | None -> 
 	(* Otherwise, if we are told to rewrite in all hypothesis via the 
            syntax "* |-", we fail iff all the different rewrites fail *) 
@@ -140,7 +144,7 @@ let general_multi_rewrite l2r c cl =
 	  | [] -> (fun gl -> error "Nothing to rewrite.")
 	  | id :: l -> 
 	      tclIFTHENTRYELSEMUST 
-		(general_rewrite_bindings_in l2r id c) 
+		(general_rewrite_bindings_in l2r id c with_evars) 
 		(do_hyps_atleastonce l)
 	in 
 	let do_hyps gl = 
@@ -150,14 +154,16 @@ let general_multi_rewrite l2r c cl =
 	      Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl)
 	  in do_hyps_atleastonce ids gl
 	in 
-	  if not cl.onconcl then do_hyps 
-	  else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps
+	  if not cl.onconcl then do_hyps else
+	    tclIFTHENTRYELSEMUST 
+	      (general_rewrite_bindings l2r c with_evars)
+	      do_hyps
 
 (* Conditional rewriting, the success of a rewriting is related 
    to the resolution of the conditions by a given tactic *)
 
 let conditional_rewrite lft2rgt tac (c,bl) = 
-  tclTHENSFIRSTn (general_rewrite_bindings lft2rgt (c,bl))
+  tclTHENSFIRSTn (general_rewrite_bindings lft2rgt (c,bl) false)
     [|tclIDTAC|] (tclCOMPLETE tac)
 
 let rewriteLR_bindings = general_rewrite_bindings true
@@ -170,7 +176,7 @@ let rewriteLRin_bindings = general_rewrite_bindings_in true
 let rewriteRLin_bindings = general_rewrite_bindings_in false
 
 let conditional_rewrite_in lft2rgt id tac (c,bl) = 
-  tclTHENSFIRSTn (general_rewrite_bindings_in lft2rgt id (c,bl))
+  tclTHENSFIRSTn (general_rewrite_bindings_in lft2rgt id (c,bl) false)
     [|tclIDTAC|] (tclCOMPLETE tac)
 
 let rewriteRL_clause = function
@@ -200,7 +206,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id -> 
 	tclTHEN 
-	  (tclTRY (general_multi_rewrite false (mkVar id,NoBindings) clause))
+	  (tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause))
 	  (clear [id]));
        tclFIRST
 	 [assumption;
@@ -1139,14 +1145,14 @@ let cond_eq_term c t gl =
     else failwith "not convertible"
   with PatternMatchingFailure -> failwith "not an equality"
 
-let rewrite_mutli_assumption_cond cond_eq_term cl gl = 
+let rewrite_multi_assumption_cond cond_eq_term cl gl = 
   let rec arec = function 
     | [] -> error "No such assumption"
     | (id,_,t) ::rest -> 
 	begin 
 	  try 
 	    let dir = cond_eq_term t gl in 
-	    general_multi_rewrite dir (mkVar id,NoBindings) cl gl
+	    general_multi_rewrite dir false (mkVar id,NoBindings) cl gl
 	  with | Failure _ | UserError _ -> arec rest
 	end
   in 
@@ -1159,7 +1165,7 @@ let replace_multi_term dir_opt c  =
       | Some true -> cond_eq_term_left c
       | Some false -> cond_eq_term_right c
   in 
-  rewrite_mutli_assumption_cond cond_eq_fun 
+  rewrite_multi_assumption_cond cond_eq_fun 
 
 (* JF. old version 
 let rewrite_assumption_cond faildir gl =
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 95cf639eee..4aae8f8905 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -25,8 +25,10 @@ open Rawterm
 open Genarg
 (*i*)
 
-val general_rewrite_bindings : bool -> constr with_bindings -> tactic
-val general_rewrite          : bool -> constr -> tactic
+val general_rewrite_bindings : 
+  bool -> constr with_bindings -> evars_flag -> tactic
+val general_rewrite : 
+  bool -> constr -> tactic
 
 (* Obsolete, use [general_rewrite_bindings l2r]
 [val rewriteLR_bindings       : constr with_bindings -> tactic]
@@ -40,12 +42,12 @@ val rewriteRL   : constr  -> tactic
 (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
 
 val general_rewrite_bindings_in :
-  bool -> identifier -> constr with_bindings -> tactic
+  bool -> identifier -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite_in          :
-  bool -> identifier -> constr -> tactic
+  bool -> identifier -> constr -> evars_flag -> tactic
 
 val general_multi_rewrite : 
-  bool -> constr with_bindings -> clause -> tactic
+  bool -> evars_flag -> constr with_bindings -> clause -> tactic
 
 val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
 val conditional_rewrite_in :
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index cb67bb2ae5..4ee02e0b82 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -401,7 +401,13 @@ VERNAC COMMAND EXTEND ImplicitTactic
 END
 
 TACTIC EXTEND apply_in
-| ["apply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in id [c] ]
+| ["apply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in false id [c] ]
 | ["apply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") 
-   "in" hyp(id) ] -> [ apply_in id (c::cl) ]
+   "in" hyp(id) ] -> [ apply_in false id (c::cl) ]
+END
+
+TACTIC EXTEND eapply_in
+| ["eapply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in true id [c] ]
+| ["epply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") 
+   "in" hyp(id) ] -> [ apply_in true id (c::cl) ]
 END
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index a940b5a0de..b8c8e6d185 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -31,7 +31,7 @@ let h_exact c        = abstract_tactic (TacExact c) (exact_check c)
 let h_exact_no_check c = abstract_tactic (TacExactNoCheck c) (exact_no_check c)
 let h_vm_cast_no_check c = 
   abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c)
-let h_apply cb       = abstract_tactic (TacApply cb) (apply_with_bindings cb)
+let h_apply ev cb    = abstract_tactic (TacApply (ev,cb)) (apply_with_bindings_gen ev cb)
 let h_elim cb cbo    = abstract_tactic (TacElim (cb,cbo)) (elim cb cbo)
 let h_elim_type c    = abstract_tactic (TacElimType c) (elim_type c)
 let h_case cb        = abstract_tactic (TacCase cb) (general_case_analysis cb)
@@ -100,7 +100,8 @@ let h_symmetry c     = abstract_tactic (TacSymmetry c) (intros_symmetry c)
 let h_transitivity c =
   abstract_tactic (TacTransitivity c) (intros_transitivity c)
 
-let h_simplest_apply c  = h_apply (c,NoBindings)
+let h_simplest_apply c  = h_apply false (c,NoBindings)
+let h_simplest_eapply c = h_apply true (c,NoBindings)
 let h_simplest_elim c   = h_elim (c,NoBindings) None
 let h_simplest_case   c = h_case (c,NoBindings)
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index bb1e4f4234..767f217b92 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -32,7 +32,7 @@ val h_exact           : constr -> tactic
 val h_exact_no_check  : constr -> tactic
 val h_vm_cast_no_check  : constr -> tactic
 
-val h_apply           : constr with_bindings -> tactic
+val h_apply           : evars_flag -> constr with_bindings -> tactic
 
 val h_elim            : constr with_bindings ->
                         constr with_bindings option -> tactic
@@ -98,6 +98,7 @@ val h_symmetry        : Tacticals.clause -> tactic
 val h_transitivity    : constr -> tactic
 
 val h_simplest_apply  : constr -> tactic 
+val h_simplest_eapply : constr -> tactic 
 val h_simplest_elim   : constr -> tactic
 val h_simplest_case   : constr -> tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e0c279a071..4e0d11e508 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -627,7 +627,7 @@ let rec intern_atomic lf ist x =
   | TacExact c -> TacExact (intern_constr ist c)
   | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
   | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
-  | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
+  | TacApply (ev,cb) -> TacApply (ev,intern_constr_with_bindings ist cb)
   | TacElim (cb,cbo) ->
       TacElim (intern_constr_with_bindings ist cb,
                option_map (intern_constr_with_bindings ist) cbo)
@@ -718,8 +718,8 @@ let rec intern_atomic lf ist x =
   | TacTransitivity c -> TacTransitivity (intern_constr ist c)
 
   (* Equality and inversion *)
-  | TacRewrite (b,c,cl) -> 
-      TacRewrite (b,intern_constr_with_bindings ist c,
+  | TacRewrite (b,ev,c,cl) -> 
+      TacRewrite (b,ev,intern_constr_with_bindings ist c,
 		  clause_app (intern_hyp_location ist) cl)
   | TacInversion (inv,hyp) ->
       TacInversion (intern_inversion_strength lf ist inv,
@@ -1994,7 +1994,7 @@ and interp_atomic ist gl = function
   | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
   | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
   | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c)
-  | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
+  | TacApply (ev,cb) -> h_apply ev (interp_constr_with_bindings ist gl cb)
   | TacElim (cb,cbo) ->
       h_elim (interp_constr_with_bindings ist gl cb)
                 (option_map (interp_constr_with_bindings ist gl) cbo)
@@ -2094,8 +2094,8 @@ and interp_atomic ist gl = function
   | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
 
   (* Equality and inversion *)
-  | TacRewrite (b,c,cl) -> 
-      Equality.general_multi_rewrite b 
+  | TacRewrite (b,ev,c,cl) -> 
+      Equality.general_multi_rewrite b ev
 	(interp_constr_with_bindings ist gl c) 
 	(interp_clause ist gl cl)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
@@ -2317,7 +2317,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacExact c -> TacExact (subst_rawconstr subst c)
   | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c)
   | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c)
-  | TacApply cb -> TacApply (subst_raw_with_bindings subst cb)
+  | TacApply (ev,cb) -> TacApply (ev,subst_raw_with_bindings subst cb)
   | TacElim (cb,cbo) ->
       TacElim (subst_raw_with_bindings subst cb,
                option_map (subst_raw_with_bindings subst) cbo)
@@ -2387,7 +2387,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
 
   (* Equality and inversion *)
-  | TacRewrite (b,c,cl) -> TacRewrite (b, subst_raw_with_bindings subst c,cl)
+  | TacRewrite (b,ev,c,cl) -> 
+      TacRewrite (b,ev,subst_raw_with_bindings subst c,cl)
   | TacInversion (DepInversion (k,c,l),hyp) ->
      TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp)
   | TacInversion (NonDepInversion _,_) as x -> x
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index defb7b7497..e71911f6b3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -341,7 +341,7 @@ let intros = tclREPEAT (intro_force false)
 
 let intro_erasing id = tclTHEN (thin [id]) (introduction id)
 
-let intros_replacing ids gls = 
+let intros_replacing ids gl = 
   let rec introrec = function
     | [] -> tclIDTAC
     | id::tl ->
@@ -350,7 +350,7 @@ let intros_replacing ids gls =
                        (intro_using id)))
            (introrec tl))
   in 
-  introrec ids gls
+  introrec ids gl
 
 (* User-level introduction tactics *)
 
@@ -504,6 +504,23 @@ let cut_in_parallel l =
   in 
     prec (List.rev l)
 
+let error_uninstantiated_metas t clenv =
+  let na = meta_name clenv.env (List.hd (Metaset.elements (metavars_of t))) in
+  let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
+  in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id)
+
+let clenv_refine_in with_evars id clenv gl =
+  let clenv = if with_evars then clenv_pose_dependent_evars clenv else clenv in
+  let new_hyp_typ  = clenv_type clenv in
+  if not with_evars & occur_meta new_hyp_typ then 
+    error_uninstantiated_metas new_hyp_typ clenv;
+  let new_hyp_prf  = clenv_value clenv in
+  tclTHEN
+    (tclEVARS (evars_of clenv.env))
+    (cut_replacing id new_hyp_typ
+      (fun x gl -> refine_no_check new_hyp_prf gl)) gl
+
+
 (****************************************************)
 (*            Resolution tactics                    *)
 (****************************************************)
@@ -576,25 +593,20 @@ let progress_with_clause innerclause clause =
   try list_try_find f ordered_metas
   with Failure _ -> error "Unable to unify"
 
-let apply_in_once gls innerclause (d,lbind) =
-  let thm = nf_betaiota (pf_type_of gls d) in
+let apply_in_once gl innerclause (d,lbind) =
+  let thm = nf_betaiota (pf_type_of gl d) in
   let rec aux clause =
     try progress_with_clause innerclause clause
     with err ->
     try aux (clenv_push_prod clause)
     with NotExtensibleClause -> raise err
-  in aux (make_clenv_binding gls (d,thm) lbind)
-
-let apply_in id lemmas gls =
-  let t' = pf_get_hyp_typ gls id in
-  let innermostclause = mk_clenv_from_n gls (Some 0) (mkVar id,t') in
-  let clause = List.fold_left (apply_in_once gls) innermostclause lemmas in
-  let new_hyp_prf  = clenv_value clause in
-  let new_hyp_typ  = clenv_type clause in
-  tclTHEN
-    (tclEVARS (evars_of clause.env))
-    (cut_replacing id new_hyp_typ
-      (fun x gls -> refine_no_check new_hyp_prf gls)) gls
+  in aux (make_clenv_binding gl (d,thm) lbind)
+
+let apply_in with_evars id lemmas gl =
+  let t' = pf_get_hyp_typ gl id in
+  let innermostclause = mk_clenv_from_n gl (Some 0) (mkVar id,t') in
+  let clause = List.fold_left (apply_in_once gl) innermostclause lemmas in
+  clenv_refine_in with_evars id clause gl
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
@@ -842,7 +854,7 @@ let simplest_elim c = default_elim (c,NoBindings)
    (e.g. it could replace id:A->B->C by id:C, knowing A/\B)
 *)
 
-let elimination_in_clause_scheme id elimclause indclause gl =
+let elimination_in_clause_scheme with_evars id elimclause indclause gl =
   let (hypmv,indmv) = 
     match clenv_independent elimclause with
         [k1;k2] -> (k1,k2)
@@ -853,18 +865,14 @@ let elimination_in_clause_scheme id elimclause indclause gl =
   let hyp_typ = pf_type_of gl hyp in
   let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain hypmv elimclause' hypclause in  
-  let new_hyp_prf  = clenv_value elimclause'' in
   let new_hyp_typ  = clenv_type elimclause'' in
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in" 
       (str "Nothing to rewrite in " ++ pr_id id);
-  tclTHEN
-    (tclEVARS (evars_of elimclause''.env))
-    (cut_replacing id new_hyp_typ
-      (fun x gls -> refine_no_check new_hyp_prf gls)) gl
+  clenv_refine_in with_evars id elimclause'' gl
 
-let general_elim_in id =
-  general_elim_clause (elimination_in_clause_scheme id)
+let general_elim_in with_evars id =
+  general_elim_clause (elimination_in_clause_scheme with_evars id)
 
 (* Case analysis tactics *)
 
@@ -2465,9 +2473,9 @@ let interpretable_as_section_decl d1 d2 = match d1,d2 with
   | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 & eq_constr t1 t2
   | (_,None,t1), (_,_,t2) -> eq_constr t1 t2
 
-let abstract_subproof name tac gls = 
+let abstract_subproof name tac gl = 
   let current_sign = Global.named_context()
-  and global_sign = pf_hyps gls in
+  and global_sign = pf_hyps gl in
   let sign,secsign = 
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) -> 
@@ -2476,8 +2484,8 @@ let abstract_subproof name tac gls =
         then (s1,push_named_context_val d s2)
 	else (add_named_decl d s1,s2)) 
       global_sign (empty_named_context,empty_named_context_val) in
-  let na = next_global_ident_away false name (pf_ids_of_hyps gls) in
-  let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
+  let na = next_global_ident_away false name (pf_ids_of_hyps gl) in
+  let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
     if occur_existential concl then
       error "\"abstract\" cannot handle existentials";
     let lemme =
@@ -2498,19 +2506,19 @@ let abstract_subproof name tac gls =
       exact_no_check 
 	(applist (lemme, 
 		 List.rev (Array.to_list (instance_from_named_context sign))))
-	gls
+	gl
 
-let tclABSTRACT name_op tac gls = 
+let tclABSTRACT name_op tac gl = 
   let s = match name_op with 
     | Some s -> s 
     | None   -> add_suffix (get_current_proof_name ()) "_subproof" 
   in  
-  abstract_subproof s tac gls
+  abstract_subproof s tac gl
 
 
-let admit_as_an_axiom gls =
+let admit_as_an_axiom gl =
   let current_sign = Global.named_context()
-  and global_sign = pf_hyps gls in
+  and global_sign = pf_hyps gl in
   let sign,secsign = 
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) -> 
@@ -2520,8 +2528,8 @@ let admit_as_an_axiom gls =
 	 else (add_named_decl d s1,s2)) 
       global_sign (empty_named_context,empty_named_context) in
   let name = add_suffix (get_current_proof_name ()) "_admitted" in
-  let na = next_global_ident_away false name (pf_ids_of_hyps gls) in
-  let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
+  let na = next_global_ident_away false name (pf_ids_of_hyps gl) in
+  let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
   if occur_existential concl then error "\"admit\" cannot handle existentials";
   let axiom =
     let cd = Entries.ParameterEntry (concl,false) in
@@ -2531,4 +2539,4 @@ let admit_as_an_axiom gls =
   exact_no_check 
     (applist (axiom, 
               List.rev (Array.to_list (instance_from_named_context sign))))
-    gls
+    gl
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c44b683f36..52c5ba8836 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -166,12 +166,13 @@ val bring_hyps : named_context -> tactic
 val apply                 : constr      -> tactic
 val apply_without_reduce  : constr      -> tactic
 val apply_list            : constr list -> tactic
-val apply_with_bindings   : constr with_bindings -> tactic
+val apply_with_bindings_gen   : evars_flag -> constr with_bindings -> tactic
+val apply_with_bindings : constr with_bindings -> tactic
 val eapply_with_bindings  : constr with_bindings -> tactic
 
 val cut_and_apply         : constr -> tactic
 
-val apply_in              : identifier -> constr with_bindings list -> tactic
+val apply_in : evars_flag -> identifier -> constr with_bindings list -> tactic
 
 (*s Elimination tactics. *)
 
@@ -226,7 +227,7 @@ val compute_elim_sig : ?elimc: (Term.constr * constr Rawterm.bindings) -> types
 
 val general_elim  :
   constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic
-val general_elim_in :
+val general_elim_in : evars_flag -> 
   identifier -> constr with_bindings -> constr with_bindings -> tactic
 
 val default_elim  : constr with_bindings -> tactic