Giving a more natural semantics to injection by default.

There were three versions of injection:

1. "injection term" without "as" clause:
   was leaving hypotheses on the goal in reverse order
2. "injection term as ipat", first version:
   was introduction hypotheses using ipat in reverse order without
   checking that the number of ipat was the size of the injection
   (activated with "Unset Injection L2R Pattern Order")
3. "injection term as ipat", second version:
   was introduction hypotheses using ipat in left-to-right order
   checking that the number of ipat was the size of the injection
   and clearing the injecting term by default if an hypothesis
   (activated with "Set Injection L2R Pattern Order", default one from 8.5)

There is now:

4. "injection term" without "as" clause, new version:
   introducing the components of the injection in the context in
   left-to-right order using default intro-patterns "?"
   and clearing the injecting term by default if an hypothesis
   (activated with "Set Structural Injection")

The new versions 3. and 4. are the "expected" ones in the sense that
they have the following good properties:
- introduction in the context is in the natural left-to-right order
- "injection" behaves the same with and without "as", always
  introducing the hypotheses in the goal what corresponds to the
  natural expectation as the changes I made in the proof scripts for
  adaptation confirm
- clear the "injection" hypothesis when an hypothesis which is the
  natural expectation as the changes I made in the proof scripts for
  adaptation confirm

The compatibility can be preserved by "Unset Structural Injection" or
by calling "simple injection".

The flag is currently off.

5 files changed, 22 insertions, 5 deletions

diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v
index 13ec5bea9..536e6fabd 100644
--- a/test-suite/bugs/closed/2016.v
+++ b/test-suite/bugs/closed/2016.v
@@ -1,6 +1,8 @@
 (* Coq 8.2beta4 *)
 Require Import Classical_Prop. 
 
+Unset Structural Injection.
+
 Record coreSemantics : Type := CoreSemantics {
   core: Type;
   corestep: core ->  core -> Prop;
@@ -49,7 +51,7 @@ unfold oe_corestep; intros.
 assert (HH:= step_fun _ _ _ H H0); clear H H0.
 destruct q1; destruct q2; unfold oe2coreSem; simpl in *.
 generalize (inj_pairT1 _ _ _ _ _ _ HH); clear HH; intros.
-injection H; clear H; intros.
+injection H.
 revert in_q1  in_corestep1 in_corestep_fun1
           H.
 pattern in_core1.
@@ -59,4 +61,4 @@ apply sym_eq.
 (** good to here **)
 Show Universes.
 Print Universes.
-Fail apply H0.
\ No newline at end of file
+Fail apply H0.
diff --git a/test-suite/bugs/closed/2021.v b/test-suite/bugs/closed/2021.v
index e598e5aed..5df92998e 100644
--- a/test-suite/bugs/closed/2021.v
+++ b/test-suite/bugs/closed/2021.v
@@ -1,6 +1,8 @@
 (* correct failure of injection/discriminate on types whose inductive
    status derives from the substitution of an argument *)
 
+Unset Structural Injection.
+
 Inductive t : nat -> Type :=
 | M : forall n: nat, nat -> t n.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_047.v b/test-suite/bugs/closed/HoTT_coq_047.v
index 29496be5e..bef3c33ca 100644
--- a/test-suite/bugs/closed/HoTT_coq_047.v
+++ b/test-suite/bugs/closed/HoTT_coq_047.v
@@ -1,3 +1,5 @@
+Unset Structural Injection.
+
 Inductive nCk : nat -> nat -> Type :=
   |zz : nCk 0 0
   | incl { m n : nat } : nCk m n -> nCk (S m) (S n)
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index c072cc641..8745cf2fb 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -4,6 +4,7 @@ Require Eqdep_dec.
 
 (* Check that Injection tries Intro until *)
 
+Unset Structural Injection.
 Lemma l1 : forall x : nat, S x = S (S x) -> False.
  injection 1.
 apply n_Sn.
@@ -37,6 +38,7 @@ intros.
  injection H.
 exact (fun H => H).
 Qed.
+Set Structural Injection.
 
 (* Test injection as *)
 
@@ -65,7 +67,7 @@ Qed.
 Goal (forall x y : nat, x = y -> S x = S y) -> True.
 intros.
 einjection (H O).
-instantiate (1:=O).
+2:instantiate (1:=O).
 Abort.
 
 Goal (forall x y : nat, x = y -> S x = S y) -> True.
@@ -85,12 +87,21 @@ Qed.
 (* Basic case, using sigT *)
 
 Scheme Equality for nat.
+Unset Structural Injection.
 Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
   existT P n H1 = existT P n H2 -> H1 = H2.
 intros.
 injection H.
 intro H0. exact H0.
 Abort.
+Set Structural Injection.
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  existT P n H1 = existT P n H2 -> H1 = H2.
+intros.
+injection H as H0.
+exact H0.
+Abort.
 
 (* Test injection using K, knowing that an equality is decidable *)
 (* Basic case, using sigT, with "as" clause *)
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 11fbf24d4..3f8a7f3eb 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -831,7 +831,7 @@ Proof.
  intro n.
  apply nat_ind with (P:= fun n => n <> S n).
  discriminate.
- red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
+ red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;auto.
 Qed.
 
 Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
@@ -1076,7 +1076,7 @@ Proof.
  simpl.
  destruct i; discriminate 1.
  destruct i; simpl;auto.
- injection 1; injection 2;intros; subst a; subst b; auto.
+ injection 1; injection 1; subst a; subst b; auto.
 Qed.
 
  Set Implicit Arguments.