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/Syntax.v') 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 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- theories/Program/Syntax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Program/Syntax.v') diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 892305b499..2fccf6249e 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*