Addressing report #3279 (inconsistency of behavior of the -> and <-

introduction patterns).

Whether we call -> and <- from assert as or apply in as, or as a
component of a larger introduction pattern, the new documented
semantics is:

- behave as subst if an equation rewriting a variable (rewrite in
  conclusion and hyps and erase variable and hyp).
- rewrite in concl if an equation not rewrite a variable or a
  quantified equality, then erase the hypothesis.

This is potential source of incompatibilities.

3 files changed, 25 insertions, 15 deletions

diff --git a/CHANGES b/CHANGES
index 26df1c13b1..257b37648b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -198,6 +198,9 @@ Tactics
 - In destruct/induction, experimental modifier "!" prefixing the
   hypothesis name to tell not erasing the hypothesis.
 - Bug fixes in "inversion as" may occasionally lead to incompatibilities.
+- Behavior of introduction patterns -> and <- made more uniform
+  (hypothesis is cleared, rewrite in hypotheses and conclusion and
+  erasing the variable when rewriting a variable).
 
 Program
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index e8ec731e61..fc6a318e6c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -783,6 +783,9 @@ the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
 \index{Introduction patterns}
 \index{Naming introduction patterns}
 \index{Disjunctive/conjunctive introduction patterns}
+\index{Disjunctive/conjunctive introduction patterns}
+\index{Equality introduction patterns}
+
 
 This extension of the tactic {\tt intros} combines introduction of
 variables or hypotheses and case analysis. An {\em introduction pattern} is
@@ -873,9 +876,10 @@ introduction pattern~$p$:
 \item introduction over {\tt ->} (respectively {\tt <-}) expects the
   hypothesis to be an equality and the right-hand-side (respectively
   the left-hand-side) is replaced by the left-hand-side (respectively
-  the right-hand-side) in both the conclusion and the context of the goal;
-  if moreover the term to substitute is a variable, the hypothesis is
-  removed;
+  the right-hand-side) in the conclusion of the goal; the hypothesis
+  itself is erased; if the term to substitute is a variable, it is
+  substituted also in the context of goal and the variable is removed
+  too;
 \item introduction over a pattern $p${\tt /{\term}} first applies
   {\term} on the hypothesis to be introduced (as in {\tt apply
   }{\term} {\tt in}), prior to the application of the introduction
@@ -1223,10 +1227,18 @@ in the list of subgoals remaining to prove.
   introduction pattern (in particular, if {\intropattern} is {\ident},
   the tactic behaves like \texttt{assert ({\ident} :\ {\form})}).
 
-  If {\intropattern} is a disjunctive/conjunctive or an equality
+  If {\intropattern} is a disjunctive/conjunctive 
   introduction pattern, the tactic behaves like \texttt{assert
-    {\form}} followed by an application of the given introduction
-  pattern to the resulting hypothesis.
+    {\form}} followed by a {\tt destruct} using this introduction pattern.
+
+  If {\intropattern} is a rewriting intropattern pattern, the tactic
+  behaves like \texttt{assert {\form}} followed by a call to {\tt
+    subst} on the resulting hypothesis, if applicable, or to {\tt
+    rewrite} otherwise.
+
+  If {\intropattern} is an injection intropattern pattern, the tactic
+  behaves like \texttt{assert {\form}} followed by {\tt injection}
+  using this introduction pattern.
 
 \item \texttt{assert {\form} as {\intropattern} by {\tac}}
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f7baed0abe..0b7edecac2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1847,17 +1847,12 @@ let rewrite_hyp assert_style l2r id =
     Hook.get forward_general_rewrite_clause l2r false (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 c =
-    tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
-  if assert_style then
-    rew_on l2r allHypsAndConcl
-  else
+  let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_type_of gl in
     let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
     let t = whd_betadeltaiota (type_of (mkVar id)) in
-    (* TODO: detect setoid equality? better detect the different equalities *)
     match match_with_equality_type t with
     | Some (hdcncl,[_;lhs;rhs]) ->
         if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
@@ -1865,16 +1860,16 @@ let rewrite_hyp assert_style l2r id =
         else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then
           subst_on l2r (destVar rhs) lhs
         else
-          Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
+          Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id]))
     | Some (hdcncl,[c]) ->
         let l2r = not l2r in (* equality of the form eq_true *)
         if isVar c then
           Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) 
 	    (Proofview.V82.tactic (clear_var_and_eq c))
         else
-          Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
+          Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id]))
     | _ ->
-        Tacticals.New.tclZEROMSG (str"Cannot find a known equation.")
+        Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id]))
   end
 
 let rec prepare_naming loc = function