]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/content_expressions.ml
sort CProp added
[helm.git] / helm / ocaml / cic_transformations / content_expressions.ml
index 2ff989da184439ef060b5344e4dcbbdbf501a89a..b913bf0de63e6ba2d28341b23188975d713b2bf6 100644 (file)
@@ -303,9 +303,10 @@ Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
  
 let string_of_sort =
   function 
-    Cic.Prop -> "Prop"
-  | Cic.Set  -> "Set"
-  | Cic.Type -> "Type"
+    Cic.Prop  -> "Prop"
+  | Cic.Set   -> "Set"
+  | Cic.Type  -> "Type"
+  | Cic.CProp -> "Type"
 ;;
 
 let get_constructors uri i =