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, 15 insertions, 0 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 17bd10fc9c..1abc393b5a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -575,3 +575,18 @@ module Huniv =
 let hcons1_univ u =
   let _,_,hdir,_,_,_ = Names.hcons_names() in
   Hashcons.simple_hcons Huniv.f hdir u
+
+
+
+(* spiwack: function for internal representation printing *)
+let string_of_universe =
+  let string_of_universe_level = function
+  | Base -> "Base"
+  | Level (path,i) -> "Level ("^Names.string_of_dir_path path^", "^string_of_int i^")"
+in
+function 
+  | Atom u -> "Atom "^string_of_universe_level u
+  | Max (l1,l2) -> "Max (["^
+               String.concat "; " (List.map string_of_universe_level l1)^"], ["^
+               String.concat "; " (List.map string_of_universe_level l2)
+               ^"])"