diff options
| author | aspiwack | 2007-12-18 12:19:12 +0000 |
|---|---|---|
| committer | aspiwack | 2007-12-18 12:19:12 +0000 |
| commit | f3eaf2869e84c942d56a7fe0cc459d9943e4b059 (patch) | |
| tree | 4a67e700f35e74324cece25f50325758e43dcb03 /kernel/names.ml | |
| parent | 0e1b31da1546b7ac0dd3664e73ba05127320bed9 (diff) | |
Nettoyage de code en vue de la release. Plus de Warning: Unused
Variable, et plus de trucs useless qui traƮnaient par ma faute (y
compris dans le noyau, la honte).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
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 c153169ab4..46a44a9b2e 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 *) |
