diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-19 17:58:43 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-19 17:58:43 +0000 |
| commit | 1f31ca099259fbea08a7fef56e1989283aec040a (patch) | |
| tree | 90064d4985a02321746c63027a8045fff9f2cb62 /toplevel/himsg.ml | |
| parent | e5ca537c17ad96529b4b39c7dbff0f25cd53b3a6 (diff) | |
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
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 4d1b608e6..70441e50d 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -471,12 +471,12 @@ let explain_pretype_error env err = (* Typeclass errors *) -let explain_unbound_class env (_,id) = - str "Unbound class name " ++ Nameops.pr_id id +let explain_not_a_class env c = + pr_constr_env env c ++ str" is not a declared type class" let explain_unbound_method env cid id = str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++ - Nameops.pr_id cid + pr_global cid let pr_constr_exprs exprs = hv 0 (List.fold_right @@ -495,7 +495,7 @@ let explain_mismatched_contexts env c i j = let explain_typeclass_error env err = match err with - | UnboundClass id -> explain_unbound_class env id + | NotAClass c -> explain_not_a_class env c | UnboundMethod (cid, id) -> explain_unbound_method env cid id | NoInstance (id, l) -> explain_no_instance env id l | MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j |