diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 40 |
1 files changed, 0 insertions, 40 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index c153169ab..46a44a9b2 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -330,43 +330,3 @@ type inv_rel_key = int (* index in the [rel_context] part of environment type id_key = inv_rel_key tableKey - - -(* spiwack : internal representation printing *) - -let string_of_identifier id = id -let string_of_module_ident id = id -let string_of_label lbl = lbl (* not public *) -let string_of_dir_path path = "["^String.concat "; " (List.map string_of_module_ident path)^"]" -let string_of_name = - function - | Name id -> "Name "^id - | Anonymous -> "Anonymous" - -let rec string_of_module_path = (* not public *) - function - | MPfile path -> "MPfile "^string_of_dir_path path - | MPbound _ -> "MPbound "^"?" (*of mod_bound_id*) - | MPself _ -> "MPself "^"?" (* of mod_self_id *) - | MPdot (mpath, lbl) -> - "MPdot ("^string_of_module_path mpath^", "^string_of_label lbl^")" - (* of module_path * label *) - -let string_of_kernel_name = (* not public *) - function - |(mpath, path, lbl) -> - "("^string_of_module_path mpath^", "^ - string_of_dir_path path^", "^ - string_of_label lbl ^")" - -let string_of_constant = string_of_kernel_name -let string_of_mutual_inductive = string_of_kernel_name -let string_of_inductive = - function - | (mind, i) -> "("^string_of_mutual_inductive mind^", "^string_of_int i^")" -let string_of_constructor = - function - | (ind, i) -> "("^string_of_inductive ind^", "^string_of_int i^")" - - -(* /spiwack *) |