CProp hierarchy is there!

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a27b0183197557d16f9782d5099580ef04274391..9e0f85b5842536f1da2466b2430850cf2adb2e06 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -247,7 +247,7 @@ let cic2grafite context menv t =
       | Cic.Meta _ -> PT.Implicit
       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
       | Cic.Sort Cic.Set -> PT.Sort `Set
-      | Cic.Sort Cic.CProp -> PT.Sort `CProp
+      | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
       | Cic.Sort Cic.Prop -> PT.Sort `Prop
       | _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None)
     in