added universes

[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index e784a8302173f188ac0d515b5cca26a29e194528..1c3ad438687b731a39a02833bcce8590c1ff6405 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -40,15 +40,17 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-let pp_literal = function  (* debugging version *)
-  | `Symbol s -> sprintf "symbol(%s)" s
-  | `Keyword s -> sprintf "keyword(%s)" s
-  | `Number s -> sprintf "number(%s)" s
-
-(* let pp_literal = function
-  | `Symbol s
-  | `Keyword s
-  | `Number s -> s *)
+let pp_literal =
+  if debug_printing then
+    (function (* debugging version *)
+      | `Symbol s -> sprintf "symbol(%s)" s
+      | `Keyword s -> sprintf "keyword(%s)" s
+      | `Number s -> sprintf "number(%s)" s)
+  else
+    (function
+      | `Symbol s
+      | `Keyword s
+      | `Number s -> s)
 
 let rec pp_term ?(pp_parens = true) t =
   let t_pp =
@@ -114,7 +116,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Num (num, _) -> num
     | Ast.Sort `Set -> "Set"
     | Ast.Sort `Prop -> "Prop"
-    | Ast.Sort `Type -> "Type"
+    | Ast.Sort (`Type _) -> "Type"
     | Ast.Sort `CProp -> "CProp"
     | Ast.Symbol (name, _) -> "'" ^ name