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
---
 pretyping/typeclasses_errors.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'pretyping/typeclasses_errors.ml')

diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 980f327cb5..1648f667ab 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -19,13 +19,14 @@ open Nametab
 open Mod_subst
 open Topconstr
 open Util
+open Libnames
 (*i*)
 
 type contexts = Parameters | Properties
 
 type typeclass_error = 
-    | UnboundClass of identifier located
-    | UnboundMethod of identifier * identifier located (* Class name, method *)
+    | NotAClass of constr
+    | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
     | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *)
 
@@ -33,7 +34,7 @@ exception TypeClassError of env * typeclass_error
 
 let typeclass_error env err = raise (TypeClassError (env, err))
 
-let unbound_class env id = typeclass_error env (UnboundClass id)
+let not_a_class env c = typeclass_error env (NotAClass c)
 
 let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 
-- 
cgit v1.2.3