- Cleanup parsing of binders, reducing to a single production for all

  binders.
- Change syntax of type class instances to better match the usual syntax of
  lemmas/definitions with name first, then arguments ":" instance.
  Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
  documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
  Program.Utils, and subset_scope as well.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 15 deletions

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 6158e88f7..6cd75257b 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(* -*- coq-prog-args: ("-emacs-U") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -13,10 +13,6 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(** Unicode lambda abstraction, does not work with factorization of lambdas. *)
-
-Notation  " 'λ' x : T , y " := (fun x:T => y) (at level 100, x,T at level 10, y at next level, no associativity) : program_scope.
-
 (** Notations for the unit type and value. *)
 
 Notation " () " := Datatypes.unit : type_scope.
@@ -42,11 +38,11 @@ Implicit Arguments cons [[A]].
 
 (** Standard notations for lists. *)
 
-Notation " [] " := nil.
-Notation " [ x ] " := (cons x nil).
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1).
+Notation " [ ] " := nil : list_scope.
+Notation " [ x ] " := (cons x nil) : list_scope.
+Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
 
-(** n-ary exists ! *)
+(** 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.
@@ -61,9 +57,3 @@ 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.
-
-(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *)
-(*   (at level 200, x ident, y ident, right associativity) : program_scope. *)
-
-(* Notation " 'Π' x : T , p " := (forall x : T, p) *)
-(*   (at level 200, x ident, right associativity) : program_scope. *)
\ No newline at end of file