diff options
| author | Maxime Dénès | 2016-10-12 15:15:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-12 15:15:33 +0200 |
| commit | d48176857632e1d2a0af0a31dc922f3c52047707 (patch) | |
| tree | 7d2ec99a1488a83fb6ec99c7b05e161407d2a4bf | |
| parent | 6e49be2c03f11f412d17e41ca2e74232d12d915c (diff) | |
| parent | 3be2307af0f1316630b46078fd6b4367c283472d (diff) | |
Merge remote-tracking branch 'github/pr/286' into v8.5
Was PR#286: Fix the definition of if_then_else for tactics with multiple
success.
| -rw-r--r-- | theories/FSets/FSetDecide.v | 19 | ||||
| -rw-r--r-- | theories/MSets/MSetDecide.v | 19 |
2 files changed, 10 insertions, 28 deletions
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 |