aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-21 13:57:23 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-21 13:57:23 +0000
commit09fc6147a76bad87d8017620c519fda2d7075a7b (patch)
tree5949af111b907feb79c8e3892b322b766ddf5ebc /pretyping/typeclasses.mli
parent2d3d9d4c7a4276fbc6bdf553f082ac12a56824d3 (diff)
Fix bug #1889, correct globalization in class declarations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11160 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses.mli')
-rw-r--r--pretyping/typeclasses.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index cb867a071..412b99e57 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -28,8 +28,8 @@ type typeclass = {
the class is a singleton. This acts as the classe's global identifier. *)
cl_impl : global_reference;
- (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the
- typeclass argument is a direct superclass. *)
+ (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
+ The boolean indicates if the typeclass argument is a direct superclass. *)
cl_context : ((global_reference * bool) option * named_declaration) list;
cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *)