Making the behavior of "injection ... as ..." more natural:

- hypotheses are introduced in the left-to-right order
- intropatterns have to match the number of generated hypotheses, and,
  if less, new introduction names are automatically generated
- clearing the hypothesis on which injection is applied, if any.

However, this is a source of incompatibilities (for a variant of
injection that is hopefully not used a lot). Compatibility can be
restored by "Unset Injection L2R Pattern Order".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16556 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 72 insertions, 23 deletions

diff --git a/CHANGES b/CHANGES
index 6e0e43478..eb39ac34e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -50,7 +50,12 @@ Tactics
   "context" can be retrieved at parse time by setting the
   "Tactic Compat Context" flag. (possible source of incompatibilities).
 - Introduction patterns of the form [x1 .. xn] or (x1,..,xn) now apply
-  injection when used on an equality statement ("ssreflect" style)
+  "injection" when used on an equality statement ("ssreflect" style).
+- Tactic "injection c as ipats" now clears c if c refers to an
+  hypothesis and moves the resulting equations in the hypotheses
+  independently of the number of ipats, which has itself to be less
+  than the number of new hypotheses (possible source of incompatibilities;
+  former behavior obtainable by "Unset Injection L2R Pattern Order").
 
 Program
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 432ff5279..238217560 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -822,6 +822,14 @@ introduction pattern~$p$:
   of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots},
   $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots}
   $p_n$]});
+\item as a special case, if the product is over an equality type, then
+  a pattern of the form {\tt [$p_{1}$ \dots\ $p_n$]} or of the form
+  {\tt ($p_1$, \ldots, $p_n$)} applies {\tt injection} instead of {\tt
+    destruct} on the hypothesis and use the patterns $p_1$, \ldots,
+  $p_n$ on the hypotheses generated by {\tt injection} (see
+  Section~\ref{injection}); if the number of patterns is smaller than
+  the number of hypotheses generated, the pattern \texttt{?} is used
+  to complete the list;
 \item introduction via {\tt ($p_1$ \& \dots\ \& $p_n$)}
   is a shortcut for introduction via
   {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
@@ -2118,7 +2126,13 @@ introduced hypothesis.
 \tacindex{injection \dots\ as}
 
 These variants apply \texttt{intros} \nelistnosep{\intropattern} after
-the call to \texttt{injection} or \texttt{einjection}.
+the call to \texttt{injection} or \texttt{einjection} so that all
+equalities generated are moved in the context of hypotheses. The
+number of {\intropattern} must not exceed the number of equalities
+newly generated. If it is smaller, fresh names are automatically
+generated to adjust the list of {\intropattern} to the number of new
+equalities. The original equality is erased if it corresponds to an
+hypothesis.
 
 \end{Variants}
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 16ab1ee5b..842ce67a0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -60,6 +60,21 @@ let _ =
       optread  = (fun () -> !discriminate_introduction);
       optwrite = (:=) discriminate_introduction }
 
+let injection_pattern_l2r_order = ref true
+
+let use_injection_pattern_l2r_order () =
+  !injection_pattern_l2r_order
+  && Flags.version_strictly_greater Flags.V8_4
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "injection left-to-right pattern order";
+      optkey   = ["Injection";"L2R";"Pattern";"Order"];
+      optread  = (fun () -> !injection_pattern_l2r_order) ;
+      optwrite = (fun b -> injection_pattern_l2r_order := b) }
+
 (* Rewriting tactics *)
 
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
@@ -1171,10 +1186,25 @@ let injEq_then tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
           (tac (clenv_value eq_clause))
 
 let injEq ipats =
+  let l2r =
+    if use_injection_pattern_l2r_order () & ipats <> None then true else false
+  in
   injEq_then
-    (fun c _ ->
-      tclTHEN (clear_if_overwritten c ipats) (intros_pattern MoveLast ipats))
-    false
+    (fun c n -> match ipats with
+      | Some ipats ->
+          let clear_tac =
+            if use_injection_pattern_l2r_order () && isVar c
+            then tclTRY (clear [destVar c])
+            else tclIDTAC in
+          let ipats =
+            if use_injection_pattern_l2r_order ()
+            then adjust_intro_patterns n ipats
+            else ipats in
+          tclTHEN
+            (clear_tac)
+            (intros_pattern MoveLast ipats)
+      | None -> tclIDTAC)
+    l2r
 
 let inj ipats with_evars = onEquality with_evars (injEq ipats)
 
@@ -1182,8 +1212,8 @@ let injClause ipats with_evars = function
   | None -> onNegatedEquality with_evars (injEq ipats)
   | Some c -> onInductionArg (inj ipats with_evars) c
 
-let injConcl gls  = injClause [] false None gls
-let injHyp id gls = injClause [] false (Some (ElimOnIdent (Loc.ghost,id))) gls
+let injConcl gls  = injClause None false None gls
+let injHyp id gls = injClause None false (Some (ElimOnIdent (Loc.ghost,id))) gls
 
 let _ = declare_injector (fun tac -> injEq_then (fun _ -> tac) true)
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 147218efd..1413c1b70 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -91,9 +91,9 @@ val discrHyp     : Id.t -> tactic
 val discrEverywhere : evars_flag -> tactic
 val discr_tac    : evars_flag ->
   constr with_bindings induction_arg option -> tactic
-val inj          : intro_pattern_expr Loc.located list -> evars_flag ->
+val inj          : intro_pattern_expr Loc.located list option -> evars_flag ->
   constr with_bindings -> tactic
-val injClause    : intro_pattern_expr Loc.located list -> evars_flag ->
+val injClause    : intro_pattern_expr Loc.located list option -> evars_flag ->
   constr with_bindings induction_arg option -> tactic
 val injHyp       : Id.t -> tactic
 val injConcl     : tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 5a8fc3bbb..75fedc598 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -118,44 +118,44 @@ let discrHyp id gl =
   discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl
 
 let injection_main c =
- elimOnConstrWithHoles (injClause []) false c
+ elimOnConstrWithHoles (injClause None) false c
 
 TACTIC EXTEND injection_main
 | [ "injection" constr_with_bindings(c) ] ->
     [ injection_main c ]
 END
 TACTIC EXTEND injection
-| [ "injection" ] -> [ injClause [] false None ]
+| [ "injection" ] -> [ injClause None false None ]
 | [ "injection" quantified_hypothesis(h) ] ->
-    [ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ]
+    [ injClause None false (Some (induction_arg_of_quantified_hyp h)) ]
 END
 TACTIC EXTEND einjection_main
 | [ "einjection" constr_with_bindings(c) ] ->
-    [ elimOnConstrWithHoles (injClause []) true c ]
+    [ elimOnConstrWithHoles (injClause None) true c ]
 END
 TACTIC EXTEND einjection
-| [ "einjection" ] -> [ injClause [] true None ]
-| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ]
+| [ "einjection" ] -> [ injClause None true None ]
+| [ "einjection" quantified_hypothesis(h) ] -> [ injClause None true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 TACTIC EXTEND injection_as_main
 | [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
-    [ elimOnConstrWithHoles (injClause ipat) false c ]
+    [ elimOnConstrWithHoles (injClause (Some ipat)) false c ]
 END
 TACTIC EXTEND injection_as
 | [ "injection" "as" simple_intropattern_list(ipat)] ->
-    [ injClause ipat false None ]
+    [ injClause (Some ipat) false None ]
 | [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
-    [ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ]
+    [ injClause (Some ipat) false (Some (induction_arg_of_quantified_hyp h)) ]
 END
 TACTIC EXTEND einjection_as_main
 | [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] ->
-    [ elimOnConstrWithHoles (injClause ipat) true c ]
+    [ elimOnConstrWithHoles (injClause (Some ipat)) true c ]
 END
 TACTIC EXTEND einjection_as
 | [ "einjection" "as" simple_intropattern_list(ipat)] ->
-    [ injClause ipat true None ]
+    [ injClause (Some ipat) true None ]
 | [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] ->
-    [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ]
+    [ injClause (Some ipat) true (Some (induction_arg_of_quantified_hyp h)) ]
 END
 
 let injHyp id gl =
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 65bf17ef0..cf9f8ee42 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -313,7 +313,7 @@ Qed.
 Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].
 Proof.
   intros a l H; remember [a] as m in H.
-  induction H; try (injection Heqm as -> ->; clear Heqm);
+  induction H; try (injection Heqm as -> ->);
     discriminate || auto.
   apply Permutation_nil in H as ->; trivial.
 Qed.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 56bdc810d..82445a0fd 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -666,7 +666,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
                      tclTRY (
                       tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     Equality.inj [] false (mkVar freshz,NoBindings);
+                     Equality.inj None false (mkVar freshz,NoBindings);
 		     intros; simpl_in_concl;
                      Auto.default_auto;
                      tclREPEAT (