- 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, 3 insertions, 15 deletions

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