From a4deb2c27bdbbba5053c0b25a326ee24a2f42e1a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 16 Mar 2008 14:50:35 +0000
Subject: Misc: Add test for bug 1704, now closed. Add usual syntax for lists
 in Program.Syntax along with stronger implicits. Update dependent induction
 test file using unicode syntax.

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

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

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index ecdacce64a..dd8536d572 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -35,6 +35,17 @@ Implicit Arguments inr [[A] [B]].
 Implicit Arguments left [[A] [B]].
 Implicit Arguments right [[A] [B]].
 
+Require Import Coq.Lists.List.
+
+Implicit Arguments nil [[A]].
+Implicit Arguments cons [[A]].
+
+(** Standard notations for lists. *)
+
+Notation " [] " := nil.
+Notation " [ x ] " := (cons x nil).
+Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..).
+
 (** n-ary exists ! *)
 
 Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p))))
-- 
cgit v1.2.3