Imported Upstream version 8.6upstream/8.6

8 files changed, 34 insertions, 41 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index eaeb2914..3c5690a7 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -24,6 +24,8 @@ Hint Extern 1 (Equivalence _) => constructor; congruence.
 
 Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
 
+Notation option_map := option_map (compat "8.4").
+
 Notation eq_dec := E.eq_dec.
 Definition eqb x y := if eq_dec x y then true else false.
 
@@ -1986,7 +1988,7 @@ Module OrdProperties (M:S).
   simpl; intros; try discriminate.
   intros.
   destruct a; destruct l; simpl in *.
-  injection H; clear H; intros; subst.
+  injection H as -> ->.
   inversion_clear H1.
   red in H; simpl in *; intuition.
   elim H0; eauto.
@@ -2050,10 +2052,10 @@ Module OrdProperties (M:S).
   generalize (elements_3 m).
   destruct (elements m).
   try discriminate.
-  destruct p; injection H; intros; subst.
-  inversion_clear H1.
+  destruct p; injection H as -> ->; intros H4.
+  inversion_clear H1 as [? ? H2|? ? H2].
   red in H2; destruct H2; simpl in *; ME.order.
-  inversion_clear H4.
+  inversion_clear H4. rename H1 into H3.
   rewrite (@InfA_alt _ eqke) in H3; eauto with *.
   apply (H3 (y,x0)); auto.
   Qed.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 13cb559b..5acdb7eb 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -8,7 +8,7 @@
 
 (** * Finite map library *)
 
-(** This file proposes an implementation of the non-dependant interface
+(** This file proposes an implementation of the non-dependent interface
  [FMapInterface.S] using lists of pairs ordered (increasing) with respect to
  left projection. *)
 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 9e59f0c5..b1c0fdaa 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -274,8 +274,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         rewrite append_assoc_1; apply in_or_app; right; apply in_cons;
           apply IHm2; auto.
         rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
-        rewrite append_neutral_r; apply in_or_app; injection H;
-          intro EQ; rewrite EQ; right; apply in_eq.
+        rewrite append_neutral_r; apply in_or_app; injection H as ->;
+          right; apply in_eq.
         rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto.
         rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
         congruence.
@@ -315,7 +315,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
          apply in_or_app.
         left; apply IHm1; auto.
         right; destruct (in_inv H0).
-         injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq.
+         injection H1 as -> ->; apply in_eq.
          apply in_cons; apply IHm2; auto.
         left; apply IHm1; auto.
         right; apply IHm2; auto.
@@ -346,7 +346,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
          apply in_or_app.
         left; apply IHm1; auto.
         right; destruct (in_inv H0).
-         injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq.
+         injection H1 as -> ->; apply in_eq.
          apply in_cons; apply IHm2; auto.
         left; apply IHm1; auto.
         right; apply IHm2; auto.
@@ -689,7 +689,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst.
   red; red; simpl.
   destruct H0.
-  injection H0; clear H0; intros _ H0; subst.
+  injection H0 as H0 _; subst.
   eapply xelements_bits_lt_1; eauto.
   apply E.bits_lt_trans with p.
   eapply xelements_bits_lt_1; eauto.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 0f11dd7a..130cbee8 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite map library *)
 
-(** This file proposes an implementation of the non-dependant interface
+(** This file proposes an implementation of the non-dependent interface
  [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *)
 
 Require Import FMapInterface.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index ad067eb3..1db6a71e 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -357,17 +357,8 @@ the above form:
         | _ => idtac
       end.
 
-    (** [if t then t1 else t2] executes [t] and, if it does not
-        fail, then [t1] will be applied to all subgoals
-        produced.  If [t] fails, then [t2] is executed. *)
-    Tactic Notation
-      "if" tactic(t)
-      "then" tactic(t1)
-      "else" tactic(t2) :=
-      first [ t; first [ t1 | fail 2 ] | t2 ].
-
     Ltac abstract_term t :=
-      if (is_var t) then fail "no need to abstract a variable"
+      tryif (is_var t) then fail "no need to abstract a variable"
       else (let x := fresh "x" in set (x := t) in *; try clearbody x).
 
     Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
       repeat (
         match goal with
         | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
-          if (change T with E.t in H) then fail
-          else if (change T with t in H) then fail
+          tryif (change T with E.t in H) then fail
+          else tryif (change T with t in H) then fail
           else clear H
         | H : ?P |- _ =>
-          if prop (FSet_Prop P) holds by
+          tryif prop (FSet_Prop P) holds by
             (auto 100 with FSet_Prop)
           then fail
           else clear H
@@ -747,7 +738,7 @@ the above form:
     | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
       contradict H; fsetdec_body
     | H: ?P -> False |- ?Q -> False =>
-      if prop (FSet_elt_Prop P) holds by
+      tryif prop (FSet_elt_Prop P) holds by
         (auto 100 with FSet_Prop)
       then (contradict H; fsetdec_body)
       else fsetdec_body
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 1f36306c..9c3ec71a 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [FSetInterface.S] using strictly ordered list. *)
 
 Require Export FSetInterface.
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index 7398c6d6..507f1cda 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.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 2ea32e97..9dbea884 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [FSetInterface.WS] using lists without redundancy. *)
 
 Require Import FSetInterface.