added universes

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

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 3d684fe39b0ff27f57fd3eb6cd23180d30042f20..0029e3db5570f95b2015211869e817257339ee20 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -116,7 +116,7 @@ let string_of_sort_kind = function
   | `Prop -> "Prop"
   | `Set -> "Set"
   | `CProp -> "CProp"
-  | `Type -> "Type"
+  | `Type _ -> "Type"
 
 let pp_ast0 t k =
   let rec aux =
@@ -275,7 +275,7 @@ let ast_of_acic0 term_info acic k =
       Hashtbl.find term_info.sort id
     with Not_found ->
       prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
-      `Type
+      `Type (CicUniv.fresh ())
   in
   let aux_substs substs =
     Some
@@ -298,13 +298,13 @@ let ast_of_acic0 term_info acic k =
     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l))
     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
-    | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type)
+    | Cic.ASort (id,Cic.Type u) ->idref id (Ast.Sort (`Type u))
     | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
     | Cic.AImplicit _ -> assert false
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type -> `Pi
+          | `Set | `Type _ -> `Pi
           | `Prop | `CProp -> `Forall
         in
         idref id (Ast.Binder (binder_kind,