diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 18:27:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-12 18:46:39 +0200 |
| commit | 0222f685ebdd55a1596d6689b96ebb86454ba1a7 (patch) | |
| tree | a4a399bd1aeed5f047ccf1ad7c40573c7384e6aa /theories/MSets | |
| parent | 112e974ec90b2afc51a7cffeba49e5777f3ea80f (diff) | |
| parent | 5dd690ee5975262d34d8dcc44191138c8d326f65 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetDecide.v | 19 |
1 files changed, 5 insertions, 14 deletions
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index f2555791b..9c622fd78 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 |