sort CProp added

[helm.git] / helm / ocaml / cic_omdoc / cic2acic.ml

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index d934e83bfa4443581c161f53ef5a5d1f80f9d79e..aa0183dad1514c05367818598267012215dcf16b 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -100,10 +100,11 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
       (*CSC: computed again and again.                               *)
       let string_of_sort t =
        match CicReduction.whd context t with 
-          C.Sort C.Prop -> "Prop"
-        | C.Sort C.Set  -> "Set"
-        | C.Sort C.Type -> "Type"
-        | _ -> assert false
+          C.Sort C.Prop  -> "Prop"
+        | C.Sort C.Set   -> "Set"
+        | C.Sort C.Type  -> "Type"
+       | C.Sort C.CProp -> "CProp"
+        | _              -> assert false
       in
        let ainnertypes,innertype,innersort,expected_available =
 (*CSC: Here we need the algorithm for Coscoy's double type-inference  *)