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

5 files changed, 17 insertions, 20 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 3354971f9b..800dc6a038 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -189,7 +189,8 @@ let lookup_utf8_tail c cs =
     | x when 0x2058 <= x & x <= 0x205E -> Utf8Symbol
     (* Invisible mathematical operators *)
     | x when 0x2061 <= x & x <= 0x2063 -> Utf8Symbol
-
+    (* utf-8 superscript U2070-207C *) 
+    | x when 0x2070 <= x & x <= 0x207C -> Utf8Symbol
     (* utf-8 subscript U2080-2089 *) 
     | x when 0x2080 <= x & x <= 0x2089 -> Utf8IdentPart n
     (* utf-8 letter-like U2100-214F *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index c87baf25fb..075077048c 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -182,7 +182,7 @@ module SearchProblem = struct
       List.length (sig_it (fst s.tacres)) + 
 	nb_empty_evars (sig_sig (fst s.tacres))
     in
-      if d <> 0 then d else
+      if d <> 0 && d <> 1 then d else
 	let pri = s.pri - s'.pri in
 	  if pri <> 0 then pri
 	  else nbgoals s - nbgoals s'
@@ -1027,7 +1027,7 @@ let require_library dirpath =
 let check_required_library d =
   let d' = List.map id_of_string d in
   let dir = make_dirpath (List.rev d') in
-  if not (Library.library_is_opened dir) then
+  if not (Library.library_is_opened dir) || not (Library.library_is_loaded dir) then
     error ("Library "^(list_last d)^" has to be required first")
 
 let init_setoid () =
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index b6fc156c39..8ce84c8271 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 184e3c3678..23f0a7d38f 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 bf37c8f231..20dfe9b01a 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. *)