- 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

4 files changed, 16 insertions, 38 deletions

diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 8ce84c827..c9de1a9e1 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -9,7 +9,7 @@
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
 
-Open Local Scope subset_scope.
+Open Local Scope program_scope.
 
 (** Tactics related to subsets and proof irrelevance. *)
 
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
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 23f0a7d38..c4a20506c 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -12,18 +12,12 @@ Require Export Coq.Program.Tactics.
 
 Set Implicit Arguments.
 
-(** Wrap a proposition inside a subset. *)
-
-Notation " {{ x }} " := (tt : { y : unit | x }).
-
 (** A simpler notation for subsets defined on a cartesian product. *)
 
 Notation "{ ( x , y )  :  A  |  P }" :=
   (sig (fun anonymous : A => let (x,y) := anonymous in P))
   (x ident, y ident, at level 10) : type_scope.
 
-(** The scope in which programs are typed (not their types). *)
-
 (** Generates an obligation to prove False. *)
 
 Notation " ! " := (False_rect _ _) : program_scope.
@@ -32,19 +26,12 @@ Delimit Scope program_scope with prg.
 
 (** Abbreviation for first projection and hiding of proofs of subset objects. *)
 
-Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : subset_scope.
-
-Delimit Scope subset_scope with subset.
-
-(* In [subset_scope] to allow masking by redefinitions for particular types. *)
-Notation "( x & ? )" := (@exist _ _ x _) : subset_scope.
+Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope.
 
 (** Coerces objects to their support before comparing them. *)
 
 Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope.
 
-(** Quantifying over subsets. *)
-
 Require Import Coq.Bool.Sumbool.
 
 (** Construct a dependent disjunction from a boolean. *)
@@ -59,10 +46,11 @@ Notation "'in_left'" := (@left _ _ _) : program_scope.
 Notation "'in_right'" := (@right _ _ _) : program_scope.
 
 (** Extraction directives *)
-
+(*
 Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
 (* Extract Inductive sigT => "prod" [ "" ]. *)
+*)
\ No newline at end of file
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 20dfe9b01..d24312ff1 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -2,7 +2,7 @@ Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
 Require Import ProofIrrelevance.
 
-Open Local Scope subset_scope.
+Open Local Scope program_scope.
 
 Implicit Arguments Enriching Acc_inv [y].
 
@@ -91,9 +91,9 @@ Section Well_founded_measure.
     
     Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
     
-    Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
-      F_sub x (fun y: { y : A | m y < m x}  => Fix_measure_F_sub (proj1_sig y) 
-        (@Acc_inv _ _ _ r (m (proj1_sig y)) (proj2_sig y))).
+    Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
+      F_sub x (fun (y : A | m y < m x)  => Fix_measure_F_sub y
+        (@Acc_inv _ _ _ r (m y) (proj2_sig y))).
     
     Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
   
@@ -102,7 +102,7 @@ Section Well_founded_measure.
   Section FixPoint.
     Variable P : A -> Type.
     
-    Variable F_sub : forall x:A, (forall (y : A | m y < m x), P (proj1_sig y)) -> P x.
+    Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x.
     
     Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
     
@@ -113,9 +113,9 @@ Section Well_founded_measure.
       forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)),
         (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
 
-    Lemma Fix_measure_F_eq :
+    Program Lemma Fix_measure_F_eq :
       forall (x:A) (r:Acc lt (m x)),
-        F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r.
+        F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r.
     Proof.
       intros x.
       set (y := m x).