CProp hierarchy is there!

[helm.git] / helm / software / components / cic_acic / cic2acic.ml

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index b039b7e5ba0405ea1ca507916eff07935c7a131c..01a4bb144c306412dd9dc8a121b046673c16f91a 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -25,19 +25,20 @@
 
 (* $Id$ *)
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe  ]
 
 let string_of_sort = function
   | `Prop -> "Prop"
   | `Set -> "Set"
   | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
-  | `CProp -> "CProp"
+  | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
+
 
 let sort_of_sort = function
   | Cic.Prop  -> `Prop
   | Cic.Set   -> `Set
   | Cic.Type u -> `Type u
-  | Cic.CProp -> `CProp
+  | Cic.CProp u -> `CProp u
 
 (* let hashtbl_add_time = ref 0.0;; *)
 
@@ -149,7 +150,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
         | C.Sort C.Set   -> `Set
         | C.Sort (C.Type u) -> `Type u
         | C.Meta _       -> `Type (CicUniv.fresh())
-        | C.Sort C.CProp -> `CProp
+        | C.Sort (C.CProp u) -> `CProp u
         | t              ->
             prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
             assert false