Processor integers + Print assumption (see coqdev mailing list for the

details).




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 38 insertions, 0 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 09c98eafc3..c153169ab4 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -332,3 +332,41 @@ 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 *)