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) --- theories/Program/Syntax.v | 7 ------- 1 file changed, 7 deletions(-) (limited to 'theories/Program') 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. -- cgit v1.2.3