From 07ffd30a82ebfe35811ca43d71aeacdb86f4cc87 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 6 Mar 2008 14:56:08 +0000
Subject: Syntax changes in typeclasses, remove "?" for usual implicit
 arguments binding, add "!" syntax for the new binders which require
 parameters and not superclasses. Change backquotes for curly braces for
 user-given implicit arguments, following tradition. This requires a hack a la
 lpar-id-coloneq. Change ident to global for typeclass names in class binders.
 Also requires a similar hack to distinguish between [ C t1 tn ] and [ c : C
 t1 tn ]. Update affected theories.

While hacking the parsing of { wf }, factorized the two versions of fix
annotation parsing that were present in g_constr and g_vernac.

Add the possibility of the user optionaly giving the priority for resolve and
exact hints (used by type classes). Syntax not fixed yet: a natural
after the list of lemmas in "Hint Resolve" syntax, a natural after a "|"
after the instance constraint in Instance declarations (ex in
Morphisms.v).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Basics.v                   | 29 +++++++++--------------------
 theories/Program/FunctionalExtensionality.v |  1 +
 2 files changed, 10 insertions(+), 20 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 8a3e5dccd9..ddc61a2dc0 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -21,11 +21,11 @@ Require Export Coq.Program.FunctionalExtensionality.
 
 Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T,y at level 10, no associativity) : program_scope.
 
-Open Scope program_scope.
+Open Local Scope program_scope.
 
-Definition id `A` := λ x : A, x.
+Definition id {A} := λ x : A, x.
 
-Definition compose `A B C` (g : B -> C) (f : A -> B) := λ x : A , g (f x).
+Definition compose {A B C} (g : B -> C) (f : A -> B) := λ x : A , g (f x).
 
 Hint Unfold compose.
 
@@ -58,11 +58,11 @@ Definition arrow (A B : Type) := A -> B.
 
 Definition impl (A B : Prop) : Prop := A -> B.
 
-Notation " f '#' x " := (f x) (at level 100, x at level 200, only parsing).
+(* Notation " f  x " := (f x) (at level 100, x at level 200, only parsing) : program_scope. *)
 
-Definition const `A B` (a : A) := fun x : B => a.
+Definition const {A B} (a : A) := fun x : B => a.
 
-Definition flip `A B C` (f : A -> B -> C) x y := f y x.
+Definition flip {A B C} (f : A -> B -> C) x y := f y x.
 
 Lemma flip_flip : forall A B C (f : A -> B -> C), flip (flip f) = f.
 Proof.
@@ -72,7 +72,7 @@ Proof.
   reflexivity.
 Qed.
 
-Definition apply `A B` (f : A -> B) (x : A) := f x.
+Definition apply {A B} (f : A -> B) (x : A) := f x.
 
 (** Notations for the unit type and value. *)
 
@@ -94,10 +94,10 @@ Implicit Arguments right [[A] [B]].
 
 (** Curryfication. *)
 
-Definition curry `a b c` (f : a -> b -> c) (p : prod a b) : c :=
+Definition curry {a b c} (f : a -> b -> c) (p : prod a b) : c :=
   let (x, y) := p in f x y.
 
-Definition uncurry `a b c` (f : prod a b -> c) (x : a) (y : b) : c :=
+Definition uncurry {a b c} (f : prod a b -> c) (x : a) (y : b) : c :=
   f (x, y).
 
 Lemma uncurry_curry : forall a b c (f : a -> b -> c), uncurry (curry f) = f.
@@ -116,17 +116,6 @@ Proof.
   destruct x ; simpl ; reflexivity.
 Qed.
 
-(** Useful implicits and notations for lists. *)
-
-Require Import Coq.Lists.List.
-
-Implicit Arguments nil [[A]].
-Implicit Arguments cons [[A]].
-
-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))))
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index e890261e12..c2a6f3df6c 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -17,6 +17,7 @@
    
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Wf.
+Require Import Coq.Program.Equality.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
-- 
cgit v1.2.3