diff options
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index d2d399f10..11c5bf398 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -29,10 +29,6 @@ open Safe_typing let strength_min l = if List.mem Local l then Local else Global -let id_of_varid c = match kind_of_term c with - | Var id -> id - | _ -> anomaly "class__id_of_varid" - (* Errors *) type coercion_error_kind = @@ -103,15 +99,6 @@ let uniform_cond nargs lt = in aux (nargs,lt) -let id_of_cl = function - | CL_FUN -> id_of_string "FUNCLASS" - | CL_SORT -> id_of_string "SORTCLASS" - | CL_CONST kn -> id_of_label (con_label kn) - | CL_IND ind -> - let (_,mip) = Global.lookup_inductive ind in - mip.mind_typename - | CL_SECVAR id -> id - let class_of_global = function | ConstRef sp -> CL_CONST sp | IndRef sp -> CL_IND sp |