From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 theories/Program/Syntax.v | 47 ++++++++++-------------------------------------
 1 file changed, 10 insertions(+), 37 deletions(-)

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

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 582bc461..61d389ed 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -1,12 +1,10 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: Syntax.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (** Custom notations and implicits for Coq prelude definitions.
 
    Author: Matthieu Sozeau
@@ -20,48 +18,23 @@ Notation " () " := tt.
 
 (** Set maximally inserted implicit arguments for standard definitions. *)
 
-Implicit Arguments Some [[A]].
-Implicit Arguments None [[A]].
-
-Implicit Arguments inl [[A] [B]] [A].
-Implicit Arguments inr [[A] [B]] [B].
-
-Implicit Arguments left [[A] [B]] [A].
-Implicit Arguments right [[A] [B]] [B].
-
-Implicit Arguments pair [[A] [B]].
-Implicit Arguments fst [[A] [B]].
-Implicit Arguments snd [[A] [B]].
-
-Require Import Coq.Lists.List.
+Arguments Some {A} _.
+Arguments None {A}.
 
-Implicit Arguments nil [[A]].
-Implicit Arguments cons [[A]].
+Arguments pair {A B} _ _.
+Arguments fst {A B} _.
+Arguments snd {A B} _.
 
-(** Standard notations for lists. *)
+Arguments nil {A}.
+Arguments cons {A} _ _.
 
-Notation " [ ] " := nil : list_scope.
-Notation " [ x ] " := (cons x nil) : list_scope.
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
-
-(** Implicit arguments for vectors. *)
+Require List.
+Export List.ListNotations.
 
 Require Import Bvector.
 
-Implicit Arguments Vnil [[A]] [].
-Implicit Arguments Vcons [[A] [n]] [].
-
 (** 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.
-
-Notation " 'exists' x y z , p" := (ex (fun x => (ex (fun y => (ex (fun z => p))))))
-  (at level 200, x ident, y ident, z ident, right associativity) : type_scope.
-
-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 "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.
-- 
cgit v1.2.3