From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 theories/Program/Syntax.v | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'theories/Program/Syntax.v')

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 6cd75257..222b5c8d 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,14 +5,15 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(* $Id: Syntax.v 11823 2009-01-21 15:32:37Z msozeau $ *)
 
-(* Custom notations and implicits for Coq prelude definitions.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
- *              91405 Orsay, France *)
+(** Custom notations and implicits for Coq prelude definitions.
 
-(** Notations for the unit type and value. *)
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(** Notations for the unit type and value à la Haskell. *)
 
 Notation " () " := Datatypes.unit : type_scope.
 Notation " () " := tt.
@@ -42,7 +42,7 @@ Notation " [ ] " := nil : list_scope.
 Notation " [ x ] " := (cons x nil) : list_scope.
 Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
 
-(** n-ary exists *)
+(** Treating n-ary exists *)
 
 Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
   (at level 200, x ident, y ident, right associativity) : type_scope.
@@ -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