X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=8b8d0361acd756e0eee840e1d9432822371e6bb8;hb=6d9de12a536ee4b9e369849ff7e9aa4ca464de9d;hp=2ff989da184439ef060b5344e4dcbbdbf501a89a;hpb=5f45c292bf9e99bd746f6ec4c7c268022012e925;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 2ff989da1..8b8d0361a 100644
--- 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 =