Do another pass on the typeclasses code. Correct globalization of class

names, gives the ability to specify qualified classes in instance
declarations. Use that in the class_tactics code. 
Refine the implementation of classes. For singleton classes the
implementation of the class becomes a regular definition (into Type or
Prop). The single method becomes a 'trivial' projection that allows to
launch typeclass resolution. Each instance is just a definition as
usual. Examples in theories/Classes/RelationClasses. This permits to
define [Class reflexive A (R : relation A) := refl : forall x, R x
x.]. The definition of [reflexive] that is generated is the same as the
original one. We just need a way to declare arbitrary lemmas as
instances of a particular class to retrofit existing reflexivity lemmas
as typeclass instances of the [reflexive] class. 
Also debug rewriting under binders in setoid_rewrite to allow rewriting
with lemmas which capture the bound variables when applied (works only
with setoid_rewrite, as rewrite first matches the lemma with the entire,
closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal
[exists x, P (f x)].


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

1 files changed, 8 insertions, 7 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8a0b940b1a..3b2b5d3d43 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -159,12 +159,12 @@ let compute_context_vars env l =
 
 let destClassApp cl =
   match cl with
-    | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
+    | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
     | _ -> raise Not_found
-
+      
 let destClassAppExpl cl =
   match cl with
-    | CApp (loc, (None,CRef (Ident f)), l) -> f, l
+    | CApp (loc, (None,CRef ref), l) -> loc, ref, l
     | _ -> raise Not_found
 
 let full_class_binders env l = 
@@ -173,12 +173,13 @@ let full_class_binders env l =
     List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
       match bk with
 	  Explicit -> 
-	    let (id, l) = destClassAppExpl cl in
+	    let (loc, id, l) = destClassAppExpl cl in
+	    let gr = Nametab.global id in
 	      (try
-		  let c = class_info (snd id) in
+		  let c = class_info gr in
 		  let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
-		    (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid
-		with Not_found -> unbound_class (Global.env ()) id)
+		    (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid
+		with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
 	| Implicit -> (x :: l', avoid))
       ([], avoid) l
   in List.rev l'