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.

6 files changed, 77 insertions, 72 deletions

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. } *)