split into two major parts:

[helm.git] / helm / ocaml / cic_transformations / content_expressions.ml

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 2ff989da184439ef060b5344e4dcbbdbf501a89a..8b8d0361acd756e0eee840e1d9432822371e6bb8 100644 (file)
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -36,7 +36,7 @@
 (* the type cexpr is inspired by OpenMath. A few primitive constructors
    have been added, in order to take into account some special features
    of functional expressions. Most notably: case, let in, let rec, and 
-   explicit substitutons *)
+   explicit substitutions *)
 
 type cexpr =
     Symbol of string option * string * subst option * string option
@@ -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 =