From 27d4a636cb7f1fbdbced1980808a9b947405eeb5 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 7 Oct 2015 23:08:45 +0200
Subject: Remove the "exists" overrides from Program. (Fix bug #4360)

---
 CHANGES                   | 2 ++
 theories/Program/Syntax.v | 7 -------
 2 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/CHANGES b/CHANGES
index 16d86c8ff1..cf2bb49271 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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 67e9a20cc1..892305b499 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.
-- 
cgit v1.2.3