From 3be2307af0f1316630b46078fd6b4367c283472d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 3 Oct 2016 13:57:16 +0200
Subject: Remove if_then_else. Use tryif instead.

if_then_else definition does not account for multi success tactics.
tryif_then_else is a primitive tactical with the expected behavior.
---
 theories/FSets/FSetDecide.v | 19 +++++--------------
 theories/MSets/MSetDecide.v | 19 +++++--------------
 2 files changed, 10 insertions(+), 28 deletions(-)

(limited to 'theories')

diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index ad067eb3d8..1db6a71e81 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/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index f2555791b2..9c622fd786 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.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 (MSet_Prop P) holds by
+          tryif prop (MSet_Prop P) holds by
             (auto 100 with MSet_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 (MSet_elt_Prop P) holds by
+      tryif prop (MSet_elt_Prop P) holds by
         (auto 100 with MSet_Prop)
       then (contradict H; fsetdec_body)
       else fsetdec_body
-- 
cgit v1.2.3


From 63ff356a8546fbcb883bb6a9711c785f75fecd41 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 12 Oct 2016 16:14:00 +0200
Subject: Little addition to 6eede071 for consistency of style in
 OrdersFacts.v.

---
 theories/Structures/OrdersFacts.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories')

diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 6f8fc1b324..0115d8a544 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -434,14 +434,14 @@ Lemma eqb_compare x y :
  (x =? y) = match compare x y with Eq => true | _ => false end.
 Proof.
 apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff.
-destruct compare; now split.
+now destruct compare.
 Qed.
 
 Lemma ltb_compare x y :
  (x <? y) = match compare x y with Lt => true | _ => false end.
 Proof.
 apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff.
-destruct compare; now split.
+now destruct compare.
 Qed.
 
 Lemma leb_compare x y :
-- 
cgit v1.2.3