Adding eintros to respect the e- prefix policy.

In pat%constr, creating new evars is now allowed only if "eintros" is
given, i.e. "intros" checks that no evars are created, and similarly
e.g. for "injection ... as ... pat%constr".

The form "eintros [...]" or "eintros ->" with the case analysis or
rewrite creating evars is now also supported.

This is not a commitment to say that it is good to have an e- modifier
to tactics. It is just to be consistent with the existing convention.

It seems to me that the "no e-" variants are good for beginners. However,
expert might prefer to use the e-variants by default. Opinions from
teachers and users would be useful.

To be possibly done: do that [= ...] work on hypotheses with side
conditions or parameters based on the idea that they apply the full
injection and not only the restriction of it to goals which are
exactly an equality, as it is today.

15 files changed, 101 insertions, 93 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index c0677d5e2a..35e6a2e317 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -144,7 +144,7 @@ type intro_pattern_naming = intro_pattern_naming_expr located
 
 type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
-  | TacIntroPattern of 'dtrm intro_pattern_expr located list
+  | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr located list
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
       ('nam * 'dtrm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 9879cfc280..321d50df38 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -310,7 +310,7 @@ let initial_atomic () =
         "hnf", TacReduce(Hnf,nocl);
         "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl);
         "compute", TacReduce(Cbv Redops.all_flags,nocl);
-        "intros", TacIntroPattern [];
+        "intros", TacIntroPattern (false,[]);
       ]
   in
   let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index cc8fd53a7f..6d4ec83f87 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -130,12 +130,12 @@ let discrHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
   discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
 
-let injection_main c =
- elimOnConstrWithHoles (injClause None) false c
+let injection_main with_evars c =
+ elimOnConstrWithHoles (injClause None) with_evars c
 
 TACTIC EXTEND injection_main
 | [ "injection" constr_with_bindings(c) ] ->
-    [ injection_main c ]
+    [ injection_main false c ]
 END
 TACTIC EXTEND injection
 | [ "injection" ] -> [ injClause None false None ]
@@ -144,7 +144,7 @@ TACTIC EXTEND injection
 END
 TACTIC EXTEND einjection_main
 | [ "einjection" constr_with_bindings(c) ] ->
-    [ elimOnConstrWithHoles (injClause None) true c ]
+    [ injection_main true c ]
 END
 TACTIC EXTEND einjection
 | [ "einjection" ] -> [ injClause None true None ]
@@ -173,7 +173,7 @@ END
 
 let injHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
-  injection_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
+  injection_main false { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma }
 
 TACTIC EXTEND dependent_rewrite
 | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index dc21fa8856..79240d2e78 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -479,8 +479,8 @@ let clause_app f = function
 let rec intern_atomic lf ist x =
   match (x:raw_atomic_tactic_expr) with
   (* Basic tactics *)
-  | TacIntroPattern l ->
-      TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
+  | TacIntroPattern (ev,l) ->
+      TacIntroPattern (ev,List.map (intern_intro_pattern lf ist) l)
   | TacApply (a,ev,cb,inhyp) ->
       TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
                 Option.map (intern_in_hyp_as ist lf) inhyp)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 4a33549f94..a418a624f9 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1644,17 +1644,17 @@ and name_atomic ?env tacexpr tac : unit Proofview.tactic =
 and interp_atomic ist tac : unit Proofview.tactic =
   match tac with
   (* Basic tactics *)
-  | TacIntroPattern l ->
+  | TacIntroPattern (ev,l) ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
-        Tacticals.New.tclWITHHOLES false 
+        Tacticals.New.tclWITHHOLES ev
         (name_atomic ~env
-          (TacIntroPattern l)
+          (TacIntroPattern (ev,l))
           (* spiwack: print uninterpreted, not sure if it is the
              expected behaviour. *)
-          (Tactics.intro_patterns l')) sigma
+          (Tactics.intro_patterns ev l')) sigma
       end }
   | TacApply (a,ev,cb,cl) ->
       (* spiwack: until the tactic is in the monad *)
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 93c5b99555..8cb07e1c22 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -136,7 +136,7 @@ let rec subst_match_goal_hyps subst = function
 
 let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
-  | TacIntroPattern l -> TacIntroPattern (List.map (subst_intro_pattern subst) l)
+  | TacIntroPattern (ev,l) -> TacIntroPattern (ev,List.map (subst_intro_pattern subst) l)
   | TacApply (a,ev,cb,cl) ->
       TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
   | TacElim (ev,cb,cbo) ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 024b51941d..a8a88d33f4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -521,9 +521,11 @@ GEXTEND Gram
     [ [
       (* Basic tactics *)
         IDENT "intros"; pl = ne_intropatterns ->
-          TacAtom (!@loc, TacIntroPattern pl)
+          TacAtom (!@loc, TacIntroPattern (false,pl))
       | IDENT "intros" ->
-          TacAtom (!@loc, TacIntroPattern [!@loc,IntroForthcoming false])
+          TacAtom (!@loc, TacIntroPattern (false,[!@loc,IntroForthcoming false]))
+      | IDENT "eintros"; pl = ne_intropatterns ->
+          TacAtom (!@loc, TacIntroPattern (true,pl))
 
       | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
           inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp))
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94530bfde2..1ff254f6ca 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -365,7 +365,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    observe_tac("h_intro_patterns ")  (let l = (List.nth intro_pats (pred i)) in 
 					       match l with 
 						 | [] -> tclIDTAC 
-						 | _ -> Proofview.V82.of_tactic (intro_patterns l));
+						 | _ -> Proofview.V82.of_tactic (intro_patterns false l));
 	    (* unfolding of all the defined variables introduced by this branch *)
 	    (* observe_tac "unfolding" pre_tac; *)
 	    (* $zeta$ normalizing of the conclusion *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f8b34e2498..bc39c93041 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -845,17 +845,18 @@ module Make
 
       (* Printing tactics as arguments *)
       let rec pr_atom0 a = tag_atom a (match a with
-        | TacIntroPattern [] -> primitive "intros"
+        | TacIntroPattern (false,[]) -> primitive "intros"
+        | TacIntroPattern (true,[]) -> primitive "eintros"
         | t -> str "(" ++ pr_atom1 t ++ str ")"
       )
 
       (* Main tactic printer *)
       and pr_atom1 a = tag_atom a (match a with
         (* Basic tactics *)
-        | TacIntroPattern [] as t ->
+        | TacIntroPattern (ev,[]) as t ->
           pr_atom0 t
-        | TacIntroPattern (_::_ as p) ->
-          hov 1 (primitive "intros" ++ spc () ++
+        | TacIntroPattern (ev,(_::_ as p)) ->
+           hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++
                     prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
         | TacApply (a,ev,cb,inhyp) ->
           hov 1 (
diff --git a/tactics/elim.ml b/tactics/elim.ml
index d59c2fba49..f2b9eec4b2 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -25,14 +25,14 @@ let introElimAssumsThen tac ba =
   (tclTHEN introElimAssums (elim_on_ba tac ba))
 
 (* Supposed to be called with a non-recursive scheme *)
-let introCaseAssumsThen tac ba =
+let introCaseAssumsThen with_evars tac ba =
   let n1 = List.length ba.Tacticals.branchsign in
   let n2 = List.length ba.Tacticals.branchnames in
   let (l1,l2),l3 =
     if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, []
     else (ba.Tacticals.branchnames, []), List.make (n1-n2) false in
   let introCaseAssums =
-    tclTHEN (intro_patterns l1) (intros_clearing l3) in
+    tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in
   (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
 
 (* The following tactic Decompose repeatedly applies the
diff --git a/tactics/elim.mli b/tactics/elim.mli
index a94f642a07..ae9cf85f3c 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -13,7 +13,7 @@ open Misctypes
 
 (** Eliminations tactics. *)
 
-val introCaseAssumsThen :
+val introCaseAssumsThen : Tacexpr.evars_flag ->
   (Tacexpr.intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
     branch_args -> unit Proofview.tactic
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 12d31d0f31..db7d2e4a13 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1383,7 +1383,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
 
 let use_clear_hyp_by_default () = false
 
-let postInjEqTac clear_flag ipats c n =
+let postInjEqTac with_evars clear_flag ipats c n =
   match ipats with
   | Some ipats ->
       let clear_tac =
@@ -1392,21 +1392,21 @@ let postInjEqTac clear_flag ipats c n =
         tclTRY (apply_clear_request clear_flag dft c) in
       let intro_tac =
         if use_injection_pattern_l2r_order ()
-        then intro_patterns_bound_to n MoveLast ipats
-        else intro_patterns_to MoveLast ipats in
+        then intro_patterns_bound_to with_evars n MoveLast ipats
+        else intro_patterns_to with_evars MoveLast ipats in
       tclTHEN clear_tac intro_tac
   | None -> apply_clear_request clear_flag false c
 
-let injEq clear_flag ipats =
+let injEq with_evars clear_flag ipats =
   let l2r =
     if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false
   in
-  injEqThen (fun c i -> postInjEqTac clear_flag ipats c i) l2r
+  injEqThen (fun c i -> postInjEqTac with_evars clear_flag ipats c i) l2r
 
-let inj ipats with_evars clear_flag = onEquality with_evars (injEq clear_flag ipats)
+let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats)
 
 let injClause ipats with_evars = function
-  | None -> onNegatedEquality with_evars (injEq None ipats)
+  | None -> onNegatedEquality with_evars (injEq with_evars None ipats)
   | Some c -> onInductionArg (inj ipats with_evars) c
 
 let injConcl = injClause None false None
@@ -1434,13 +1434,13 @@ let dEq with_evars =
   dEqThen with_evars (fun clear_flag c x ->
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
-let intro_decompe_eq tac data cl =
+let intro_decomp_eq tac data cl =
   Proofview.Goal.enter { enter = begin fun gl ->
     let cl = pf_apply make_clenv_binding gl cl NoBindings in
     decompEqThen (fun _ -> tac) data cl
   end }
 
-let _ = declare_intro_decomp_eq intro_decompe_eq
+let _ = declare_intro_decomp_eq intro_decomp_eq
 
 (* [subst_tuple_term dep_pair B]
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 3707ef90b4..852c2ee7cb 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -465,7 +465,7 @@ let raw_inversion inv_kind id status names =
       (tclTHENS
         (assert_before Anonymous cut_concl)
         [case_tac names
-            (introCaseAssumsThen
+            (introCaseAssumsThen false (* ApplyOn not supported by inversion *)
                (rewrite_equations_tac as_mode inv_kind id neqns))
             (Some elim_predicate) ind (c, t);
         onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2f24e55a57..61a0850c27 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1416,6 +1416,7 @@ let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
         general_case_analysis_in_context with_evars clear_flag cx
 
 let simplest_case c = general_case_analysis false None (c,NoBindings)
+let simplest_ecase c = general_case_analysis true None (c,NoBindings)
 
 (* Elimination tactic with bindings but using the default elimination
  * constant associated with the type. *)
@@ -2241,7 +2242,7 @@ let intro_decomp_eq loc l thin tac id =
     Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
   end }
 
-let intro_or_and_pattern loc bracketed ll thin tac id =
+let intro_or_and_pattern loc with_evars bracketed ll thin tac id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
@@ -2251,14 +2252,14 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
   let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
   let ll = get_and_check_or_and_pattern loc ll branchsigns in
   Tacticals.New.tclTHENLASTn
-    (Tacticals.New.tclTHEN (simplest_case c) (clear [id]))
+    (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
     (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
        nv_with_let ll)
   end }
 
-let rewrite_hyp_then assert_style thin l2r id tac =
+let rewrite_hyp_then assert_style with_evars thin l2r id tac =
   let rew_on l2r =
-    Hook.get forward_general_rewrite_clause l2r false (mkVar id,NoBindings) in
+    Hook.get forward_general_rewrite_clause l2r with_evars (mkVar id,NoBindings) in
   let subst_on l2r x rhs =
     Hook.get forward_subst_one true x (id,rhs,l2r) in
   let clear_var_and_eq id' = clear [id';id] in
@@ -2369,12 +2370,13 @@ let exceed_bound n = function
      [patl]: introduction patterns to interpret
   *)
 
-let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
+let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
+  function
   | [] when fit_bound n bound ->
       tac ids thin
   | [] ->
       (* Behave as IntroAnonymous *)
-      intro_patterns_core b avoid ids thin destopt bound n tac
+      intro_patterns_core with_evars b avoid ids thin destopt bound n tac
         [dloc,IntroNaming IntroAnonymous]
   | (loc,pat) :: l ->
   if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
@@ -2382,48 +2384,49 @@ let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
   | IntroForthcoming onlydeps ->
       intro_forthcoming_then_gen (NamingAvoid (avoid@explicit_intro_names l))
 	  destopt onlydeps n bound
-        (fun ids -> intro_patterns_core b avoid ids thin destopt bound
+        (fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound
           (n+List.length ids) tac l)
   | IntroAction pat ->
       intro_then_gen (make_tmp_naming avoid l pat)
 	destopt true false
-        (intro_pattern_action loc (b || not (List.is_empty l)) false pat thin
-          destopt
-          (fun thin bound' -> intro_patterns_core b avoid ids thin destopt bound' 0
+        (intro_pattern_action loc with_evars (b || not (List.is_empty l)) false
+          pat thin destopt
+          (fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0
             (fun ids thin ->
-              intro_patterns_core b avoid ids thin destopt bound (n+1) tac l)))
+              intro_patterns_core with_evars b avoid ids thin destopt bound (n+1) tac l)))
   | IntroNaming pat ->
-      intro_pattern_naming loc b avoid ids pat thin destopt bound (n+1) tac l
+      intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound (n+1) tac l
 
   (* Pi-introduction rule, used backwards *)
-and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l =
+and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac l =
   match pat with
   | IntroIdentifier id ->
       check_thin_clash_then id thin avoid (fun thin ->
         intro_then_gen (NamingMustBe (loc,id)) destopt true false
-          (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l))
+          (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l))
   | IntroAnonymous ->
       intro_then_gen (NamingAvoid (avoid@explicit_intro_names l))
 	destopt true false
-        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
+        (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
   | IntroFresh id ->
       (* todo: avoid thinned names to interfere with generation of fresh name *)
       intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l))
 	destopt true false
-        (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
+        (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
 
-and intro_pattern_action loc b style pat thin destopt tac id = match pat with
+and intro_pattern_action loc with_evars b style pat thin destopt tac id =
+  match pat with
   | IntroWildcard ->
       tac ((loc,id)::thin) None []
   | IntroOrAndPattern ll ->
-      intro_or_and_pattern loc b ll thin tac id
+      intro_or_and_pattern loc with_evars b ll thin tac id
   | IntroInjection l' ->
       intro_decomp_eq loc l' thin tac id
   | IntroRewrite l2r ->
-      rewrite_hyp_then style thin l2r id (fun thin -> tac thin None [])
+      rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None [])
   | IntroApplyOn (f,(loc,pat)) ->
       let naming,tac_ipat =
-        prepare_intros_loc loc (IntroIdentifier id) destopt pat in
+        prepare_intros_loc loc with_evars (IntroIdentifier id) destopt pat in
       let doclear =
         if naming = NamingMustBe (loc,id) then
           Proofview.tclUNIT () (* apply_in_once do a replacement *)
@@ -2433,48 +2436,48 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
         let Sigma (c, sigma, p) = f.delayed env sigma in
         Sigma ((c, NoBindings), sigma, p)
       } in
-      apply_in_delayed_once false true true true naming id (None,(loc,f))
+      apply_in_delayed_once false true true with_evars naming id (None,(loc,f))
         (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
 
-and prepare_intros_loc loc dft destopt = function
+and prepare_intros_loc loc with_evars dft destopt = function
   | IntroNaming ipat ->
       prepare_naming loc ipat,
       (fun id -> move_hyp id destopt)
   | IntroAction ipat ->
       prepare_naming loc dft,
       (let tac thin bound =
-        intro_patterns_core true [] [] thin destopt bound 0
+        intro_patterns_core with_evars true [] [] thin destopt bound 0
           (fun _ l -> clear_wildcards l) in
-      fun id -> intro_pattern_action loc true true ipat [] destopt tac id)
+      fun id ->
+        intro_pattern_action loc with_evars true true ipat [] destopt tac id)
   | IntroForthcoming _ -> user_err_loc
       (loc,"",str "Introduction pattern for one hypothesis expected.")
 
-let intro_patterns_bound_to n destopt =
-  intro_patterns_core true [] [] [] destopt
+let intro_patterns_bound_to with_evars n destopt =
+  intro_patterns_core with_evars true [] [] [] destopt
     (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
 
-let intro_patterns_to destopt l =
-  (* Eta-expansion because of a side-effect *)
-  intro_patterns_core (use_bracketing_last_or_and_intro_pattern ())
-    [] [] [] destopt None 0 (fun _ l -> clear_wildcards l) l
+let intro_patterns_to with_evars destopt =
+  intro_patterns_core with_evars (use_bracketing_last_or_and_intro_pattern ())
+    [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
 
-let intro_pattern_to destopt pat =
-  intro_patterns_to destopt [dloc,pat]
+let intro_pattern_to with_evars destopt pat =
+  intro_patterns_to with_evars destopt [dloc,pat]
 
-let intro_patterns = intro_patterns_to MoveLast
+let intro_patterns with_evars = intro_patterns_to with_evars MoveLast
 
 (* Implements "intros" *)
-let intros_patterns = function
+let intros_patterns with_evars = function
   | [] -> intros
-  | l -> intro_patterns_to MoveLast l
+  | l -> intro_patterns_to with_evars MoveLast l
 
 (**************************)
 (*   Forward reasoning    *)
 (**************************)
 
-let prepare_intros dft destopt = function
+let prepare_intros with_evars dft destopt = function
   | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
-  | Some (loc,ipat) -> prepare_intros_loc loc dft destopt ipat
+  | Some (loc,ipat) -> prepare_intros_loc loc with_evars dft destopt ipat
 
 let ipat_of_name = function
   | Anonymous -> None
@@ -2485,7 +2488,7 @@ let head_ident c =
    if isVar c then Some (destVar c) else None
 
 let assert_as first hd ipat t =
-  let naming,tac = prepare_intros IntroAnonymous MoveLast ipat in
+  let naming,tac = prepare_intros false IntroAnonymous MoveLast ipat in
   let repl = do_replace hd naming in
   let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in
   if first then assert_before_then_gen repl naming t tac
@@ -2502,7 +2505,8 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
   let destopt =
     if with_evars then MoveLast (* evars would depend on the whole context *)
     else get_previous_hyp_position id gl in
-  let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in
+  let naming,ipat_tac =
+    prepare_intros with_evars (IntroIdentifier id) destopt ipat in
   let lemmas_target, last_lemma_target =
     let last,first = List.sep_last lemmas in
     List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last)
@@ -2979,19 +2983,19 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
     (intros_move rstatus)
     (intros_move newlstatus)
 
-let dest_intro_patterns avoid thin dest pat tac =
-  intro_patterns_core true avoid [] thin dest None 0 tac pat
+let dest_intro_patterns with_evars avoid thin dest pat tac =
+  intro_patterns_core with_evars true avoid [] thin dest None 0 tac pat
 
-let safe_dest_intro_patterns avoid thin dest pat tac =
+let safe_dest_intro_patterns with_evars avoid thin dest pat tac =
   Proofview.tclORELSE
-    (dest_intro_patterns avoid thin dest pat tac)
+    (dest_intro_patterns with_evars avoid thin dest pat tac)
     begin function (e, info) -> match e with
       | UserError ("move_hyp",_) ->
        (* May happen e.g. with "destruct x using s" with an hypothesis
           which is morally an induction hypothesis to be "MoveLast" if
           known as such but which is considered instead as a subterm of
           a constructor to be move at the place of x. *)
-          dest_intro_patterns avoid thin MoveLast pat tac
+          dest_intro_patterns with_evars avoid thin MoveLast pat tac
       | e -> Proofview.tclZERO ~info e
     end
 
@@ -3023,7 +3027,7 @@ let get_recarg_dest (recargdests,tophyp) =
    had to be introduced at the top of the context).
 *)
 
-let induct_discharge dests avoid' tac (avoid,ra) names =
+let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
   let avoid = avoid @ avoid' in
   let rec peel_tac ra dests names thin =
     match ra with
@@ -3036,12 +3040,12 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 	      (pat, [dloc, IntroNaming (IntroIdentifier id')])
           | _ -> consume_pattern avoid (Name recvarname) deprec gl names in
         let dest = get_recarg_dest dests in
-        dest_intro_patterns avoid thin dest [recpat] (fun ids thin ->
+        dest_intro_patterns with_evars avoid thin dest [recpat] (fun ids thin ->
         Proofview.Goal.enter { enter = begin fun gl ->
           let (hyprec,names) =
             consume_pattern avoid (Name hyprecname) depind gl names
           in
-	  dest_intro_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
+	  dest_intro_patterns with_evars avoid thin MoveLast [hyprec] (fun ids' thin ->
 	    peel_tac ra' (update_dest dests ids') names thin)
         end })
         end }
@@ -3050,7 +3054,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
         let pat,names =
           consume_pattern avoid (Name hyprecname) dep gl names in
-	dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin ->
+	dest_intro_patterns with_evars avoid thin MoveLast [pat] (fun ids thin ->
         peel_tac ra' (update_dest dests ids) names thin)
         end }
     | (RecArg,_,dep,recvarname) :: ra' ->
@@ -3058,14 +3062,14 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
         let (pat,names) =
           consume_pattern avoid (Name recvarname) dep gl names in
         let dest = get_recarg_dest dests in
-	dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
+	dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
         peel_tac ra' dests names thin)
         end }
     | (OtherArg,_,dep,_) :: ra' ->
         Proofview.Goal.enter { enter = begin fun gl ->
         let (pat,names) = consume_pattern avoid Anonymous dep gl names in
         let dest = get_recarg_dest dests in
-	safe_dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
+	safe_dest_intro_patterns with_evars avoid thin dest [pat] (fun ids thin ->
         peel_tac ra' dests names thin)
         end }
     | [] ->
@@ -4052,7 +4056,7 @@ let induction_tac with_evars params indvars elim =
    hypotheses from the context, replacing the main hypothesis on which
    induction applies with the induction hypotheses *)
 
-let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
+let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_tac =
   let open Context.Named.Declaration in
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
@@ -4082,7 +4086,8 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
         Tacticals.New.tclMAP expand_hyp toclear;
       ])
       (Array.map2
-         (induct_discharge lhyp0 avoid (re_intro_dependent_hypotheses statuslists))
+         (induct_discharge with_evars lhyp0 avoid
+            (re_intro_dependent_hypotheses statuslists))
          indsign names)
     in
     Sigma.Unsafe.of_pair (tac, sigma)
@@ -4092,7 +4097,7 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyp
   Proofview.Goal.enter { enter = begin fun gl ->
   let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in
   atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
-    apply_induction_in_context (Some hyp0) inhyps (pi3 elim_info) indvars names
+    apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names
       (fun elim -> induction_tac with_evars [] [hyp0] elim))
   end }
 
@@ -4141,7 +4146,7 @@ let induction_without_atomization isrec with_evars elim names lid =
     induction_tac with_evars params realindvars elim;
   ] in
   let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in
-  apply_induction_in_context None [] elim indvars names induct_tac
+  apply_induction_in_context with_evars None [] elim indvars names induct_tac
   end }
 
 (* assume that no occurrences are selected *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 142fdd3ebc..e346a0d566 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -102,16 +102,16 @@ val use_clear_hyp_by_default : unit -> bool
 
 (** {6 Introduction tactics with eliminations. } *)
 
-val intro_patterns : intro_patterns -> unit Proofview.tactic
-val intro_patterns_to : Id.t move_location -> intro_patterns ->
+val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic
+val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns ->
   unit Proofview.tactic
-val intro_patterns_bound_to : int -> Id.t move_location -> intro_patterns ->
+val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns ->
   unit Proofview.tactic
-val intro_pattern_to : Id.t move_location -> delayed_open_constr intro_pattern_expr ->
+val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr ->
   unit Proofview.tactic
 
 (** Implements user-level "intros", with [] standing for "**" *)
-val intros_patterns : intro_patterns -> unit Proofview.tactic
+val intros_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic
 
 (** {6 Exact tactics. } *)