diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-10-07 23:08:45 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-10-07 23:08:45 +0200 |
| commit | 27d4a636cb7f1fbdbced1980808a9b947405eeb5 (patch) | |
| tree | 830d7de2466f41ec69fe6792b7f0e3d85acefa5a | |
| parent | e26b4dbedd29acbfb9cbf2320193cc68afa60cf3 (diff) | |
Remove the "exists" overrides from Program. (Fix bug #4360)
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 7 |
2 files changed, 2 insertions, 7 deletions
@@ -28,6 +28,8 @@ Tactics "intros" automatically complete the introduction of its subcomponents, as the the disjunctive-conjunctive introduction patterns in non-terminal position already do. +- Importing Program no longer overrides the "exists" tactic (potential source + of incompatibilities). API diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 67e9a20cc..892305b49 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -32,10 +32,3 @@ Require List. Export List.ListNotations. Require Import Bvector. - -(** Treating n-ary exists *) - -Tactic Notation "exists" constr(x) := exists x. -Tactic Notation "exists" constr(x) constr(y) := exists x ; exists y. -Tactic Notation "exists" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. -Tactic Notation "exists" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. |