more work

[helm.git] / helm / software / components / ng_kernel / nCicPp.ml

diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml
index cde028be4417b58b8985607368e1f18a4875912b..cebdaf0b29908916a601c04756058aed1d1c8450 100644 (file)
--- a/helm/software/components/ng_kernel/nCicPp.ml
+++ b/helm/software/components/ng_kernel/nCicPp.ml
@@ -137,7 +137,7 @@ let ppterm ~context ~subst ~metasenv:_ ?(inside_fix=false) t =
           end;
         F.fprintf f "])"
    | C.Sort C.Prop -> F.fprintf f "Prop"
-   | C.Sort (C.Type []) -> F.fprintf f "IllFormedUniverse"
+   | C.Sort (C.Type []) -> F.fprintf f "Type0"
    | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u)
    | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u)
    | C.Sort (C.Type l) ->