Universes introduction

[helm.git] / helm / ocaml / cic_proof_checking / cicPp.ml

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 5c5bd71fff473b8522256c633a0fa7c5e9546c74..8172b47f7ac92ce9a9fdee3fada7775cc048c84d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -69,7 +69,7 @@ let rec pp t l =
          (match get_nth l n with
              Some (C.Name s) -> s
            | Some C.Anonymous -> "__" ^ string_of_int n
-           | _ -> raise CicPpInternalError
+           | None -> "_hidden_" ^ string_of_int n
          )
         with
          NotEnoughElements -> string_of_int (List.length l - n)
@@ -85,10 +85,10 @@ let rec pp t l =
        (match s with
            C.Prop  -> "Prop"
          | C.Set   -> "Set"
-         | C.Type  -> "Type"
+         | C.Type _ -> "Type" (* TASSI: universe is not explicit *)
         | C.CProp -> "CProp" 
        )
-    | C.Implicit -> "?"
+    | C.Implicit _ -> "?"
     | C.Prod (b,s,t) ->
        (match b with
           C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)