From 1f31ca099259fbea08a7fef56e1989283aec040a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 19 Mar 2008 17:58:43 +0000
Subject: 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
---
 interp/implicit_quantifiers.ml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

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'
-- 
cgit v1.2.3