Minor fixes:

- Allow unicode superscripts characters.
- Put Program notations in scopes.
- Correct priority semantics in typeclasses eauto.


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

3 files changed, 13 insertions, 17 deletions

diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index b6fc156c3..8ce84c827 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -9,6 +9,8 @@
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
 
+Open Local Scope subset_scope.
+
 (** Tactics related to subsets and proof irrelevance. *)
 
 (** Simplify dependent equality using sigmas to equality of the codomains if possible. *)
@@ -72,7 +74,7 @@ Ltac clear_subset_proofs :=
 
 Ltac pi := repeat progress f_equal ; apply proof_irrelevance.
 
-Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> (`n) = (`m).
+Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m.
 Proof.
   induction n.
   induction m.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 184e3c367..23f0a7d38 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -22,17 +22,17 @@ Notation "{ ( x , y )  :  A  |  P }" :=
   (sig (fun anonymous : A => let (x,y) := anonymous in P))
   (x ident, y ident, at level 10) : type_scope.
 
-(** Generates an obligation to prove False. *)
-
-Notation " ! " := (False_rect _ _).
+(** The scope in which programs are typed (not their types). *)
 
-(** Abbreviation for first projection and hiding of proofs of subset objects. *)
+(** Generates an obligation to prove False. *)
 
-(** The scope in which programs are typed (not their types). *)
+Notation " ! " := (False_rect _ _) : program_scope.
 
 Delimit Scope program_scope with prg.
 
-Notation " ` t " := (proj1_sig t) (at level 10) : core_scope.
+(** 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.
 
@@ -41,23 +41,15 @@ Notation "( x & ? )" := (@exist _ _ x _) : subset_scope.
 
 (** Coerces objects to their support before comparing them. *)
 
-Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).
+Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope.
 
 (** Quantifying over subsets. *)
 
-(* Notation "'fun' ( x : A | P ) => Q" := *)
-(*   (fun (x :A|P} => Q) *)
-(*   (at level 200, x ident, right associativity). *)
-
-(* Notation "'forall' ( x : A | P ), Q" := *)
-(*   (forall (x : A | P), Q) *)
-(*   (at level 200, x ident, right associativity). *)
-
 Require Import Coq.Bool.Sumbool.
 
 (** Construct a dependent disjunction from a boolean. *)
 
-Notation "'dec'" := (sumbool_of_bool) (at level 0). 
+Notation dec := sumbool_of_bool.
 
 (** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index bf37c8f23..20dfe9b01 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -2,6 +2,8 @@ Require Import Coq.Init.Wf.
 Require Import Coq.Program.Utils.
 Require Import ProofIrrelevance.
 
+Open Local Scope subset_scope.
+
 Implicit Arguments Enriching Acc_inv [y].
 
 (** Reformulation of the Wellfounded module using subsets where possible. *)