raise uncertain when a sort is not a sort but may be, use max for mixing universes...

[helm.git] / helm / software / components / content_pres / termContentPres.ml

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 378708bce764e9e0e8010ff5b64e696f9e52f7eb..d6694cbb66419be45f3c88609c12f6434e4eef62 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -93,6 +93,7 @@ let string_of_sort_kind = function
   | `Set -> "Set"
   | `CProp _ -> "CProp"
   | `Type _ -> "Type"
+  | `NType s -> "Type[" ^ s ^ "]"
 
 let pp_ast0 t k =
   let rec aux =
@@ -598,6 +599,8 @@ let instantiate_level2 env term =
     | Ast.Magic magic -> aux_magic env magic
     | Ast.Variable var -> aux_variable env var
 
+    | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
+
     | _ -> assert false
   and aux_opt env = function
     | Some term -> Some (aux env term)