diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-01 14:02:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-01 14:02:59 +0000 |
| commit | 7b6ed1e95bef26f4ae85d7471985128c0dfdbc15 (patch) | |
| tree | a2beab552c8e57d5db2833494e5cc79e6374cc84 /pretyping/classops.ml | |
| parent | 2a9a43be51ac61e04ebf3fce902899155b48057f (diff) | |
Déplacement de qualid dans Nametab, hors du noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/classops.ml')
| -rwxr-xr-x | pretyping/classops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index ca8553525..630a8bb31 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -232,9 +232,9 @@ let strength_of_cl = function let string_of_class = function | CL_FUN -> "FUNCLASS" | CL_SORT -> "SORTCLASS" - | CL_CONST sp -> string_of_qualid (Global.qualid_of_global (ConstRef sp)) - | CL_IND sp -> string_of_qualid (Global.qualid_of_global (IndRef sp)) - | CL_SECVAR sp -> string_of_qualid (Global.qualid_of_global (VarRef sp)) + | CL_CONST sp -> Global.string_of_global (ConstRef sp) + | CL_IND sp -> Global.string_of_global (IndRef sp) + | CL_SECVAR sp -> Global.string_of_global (VarRef sp) (* coercion_value : int -> unsafe_judgment * bool *) |