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

11 files changed, 109 insertions, 93 deletions

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