Modifying theories to preferably use the "[= ]" syntax, and,

sometimes, to use "intros [= ...]" rather than things like "intros H;
injection H as [= ...]".

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>

2 files changed, 15 insertions, 15 deletions

diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index a726eebd31..330c7959ac 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -910,10 +910,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 as <-. apply Hp.
+          intros p Hp x [= <-]. apply Hp.
            reflexivity.
           intros _ x. revert IHr. case choose.
-            intros p Hp H. injection H as <-. apply Hp.
+            intros p Hp [= <-]. apply Hp.
             reflexivity.
             intros. discriminate.
   Qed.
@@ -970,11 +970,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 as <-. apply IHl. reflexivity.
+       injection H as [= <-]. apply IHl. reflexivity.
        destruct o; simpl.
-         injection H as <-. reflexivity.
+         injection H as [= <-]. reflexivity.
          destruct (min_elt r); simpl in *.
-           injection H as <-. apply IHr. reflexivity.
+           injection H as [= <-]. apply IHr. reflexivity.
            discriminate.
   Qed.
 
@@ -998,15 +998,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 as <-.
+        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_spec3 in Hp.
         destruct o.
-          injection H as <-. intros Hl.
+          injection H as [= <-]. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (min_elt r).
-            injection H as <-.
+            injection H as [= <-].
             destruct y as [z|z|].
               apply (IHr e z); trivial.
               elim (Hp _ H').
@@ -1023,11 +1023,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 as <-. apply IHr. reflexivity.
+       injection H as [= <-]. apply IHr. reflexivity.
        destruct o; simpl.
-         injection H as <-. reflexivity.
+         injection H as [= <-]. reflexivity.
          destruct (max_elt l); simpl in *.
-           injection H as <-. apply IHl. reflexivity.
+           injection H as [= <-]. apply IHl. reflexivity.
            discriminate.
   Qed.
 
@@ -1051,15 +1051,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 as <-.
+        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_spec3 in Hp.
         destruct o.
-          injection H as <-. intros Hl.
+          injection H as [= <-]. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (max_elt l).
-            injection H as <-.
+            injection H as [= <-].
             destruct y as [z|z|].
               elim (Hp _ H').
               apply (IHl e z); trivial.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index f9105fdf74..a2ffd2050e 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -1950,7 +1950,7 @@ Module Make (X: Orders.OrderedType) <:
  generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs).
  set (P := Raw.remove_min_ok s). clearbody P.
  destruct (Raw.remove_min s) as [(x0,s0)|]; try easy.
- intros H U. injection U as -> <-. simpl.
+ intros H [= -> <-]. simpl.
  destruct (H x s0); auto. subst; intuition.
  Qed.