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.

1 files changed, 14 insertions, 14 deletions

diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index 7398c6d65..507f1cda6 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -1007,10 +1007,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       destruct o.
         intros x H. injection H; intros; subst. reflexivity.
         revert IHl. case choose.
-          intros p Hp x H. injection H; intros; subst; clear H. apply Hp.
+          intros p Hp x H. injection H as <-. apply Hp.
            reflexivity.
           intros _ x. revert IHr. case choose.
-            intros p Hp H. injection H; intros; subst; clear H. apply Hp.
+            intros p Hp H. injection H as <-. apply Hp.
             reflexivity.
             intros. discriminate.
   Qed.
@@ -1066,11 +1066,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (min_elt l); intros.
-       injection H. intros <-. apply IHl. reflexivity.
+       injection H as <-. apply IHl. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (min_elt r); simpl in *.
-           injection H. intros <-. apply IHr. reflexivity.
+           injection H as <-. apply IHr. reflexivity.
            discriminate.
   Qed.
 
@@ -1094,15 +1094,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (min_elt l).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
         intro Hp; rewrite Hp in H. apply min_elt_3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (min_elt r).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               apply (IHr e z); trivial.
               elim (Hp _ H').
@@ -1119,11 +1119,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (max_elt r); intros.
-       injection H. intros <-. apply IHr. reflexivity.
+       injection H as <-. apply IHr. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (max_elt l); simpl in *.
-           injection H. intros <-. apply IHl. reflexivity.
+           injection H as <-. apply IHl. reflexivity.
            discriminate.
   Qed.
 
@@ -1147,15 +1147,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (max_elt r).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
         intro Hp; rewrite Hp in H. apply max_elt_3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (max_elt l).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               elim (Hp _ H').
               apply (IHl e z); trivial.