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

3 files changed, 49 insertions, 19 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 16ab1ee5b4..842ce67a0d 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 147218efd4..1413c1b70f 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 5a8fc3bbb8..75fedc5985 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 =