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.

5 files changed, 13 insertions, 13 deletions

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) ->