aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/class.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-18 17:09:31 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-18 17:09:31 +0000
commitaa37087b8e7151ea96321a11012c1064210ef4ea (patch)
treefff9ed837668746545832e3bd9f0a6dd99936ee4 /toplevel/class.ml
parentf61e682857596f0274b956295efd2bfba63bc8c0 (diff)
Modulification of Label
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/class.ml')
-rw-r--r--toplevel/class.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 01205e597..6f0ac1793 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -164,8 +164,8 @@ let get_strength stre ref cls clt =
let ident_key_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
- | CL_CONST sp -> string_of_label (con_label sp)
- | CL_IND (sp,_) -> string_of_label (mind_label sp)
+ | CL_CONST sp -> Label.to_string (con_label sp)
+ | CL_IND (sp,_) -> Label.to_string (mind_label sp)
| CL_SECVAR id -> Id.to_string id
(* coercion identité *)