From 0deeb743b6b90b7be64d150c142ed5ef77d77943 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 21 Jan 2009 12:53:33 +0000
Subject: - Better deal with commands inside section titles in latex output
 using the support from hyperref. - Rename n-ary 'exist' tactic to 'exists' in
 Program.Syntax.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11821 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Syntax.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index f45511823d..25f6a5152f 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -53,7 +53,7 @@ Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p)))
 Notation " 'exists' x y z w , p" := (ex (fun x => (ex (fun y => (ex (fun z => (ex (fun w => p))))))))
   (at level 200, x ident, y ident, z ident, w ident, right associativity) : type_scope.
 
-Tactic Notation "exist" constr(x) := exists x.
-Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
-Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
-Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
+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