X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=9e0f85b5842536f1da2466b2430850cf2adb2e06;hb=393187c5f5a6e71d467ab04b65f3a935701724fb;hp=a27b0183197557d16f9782d5099580ef04274391;hpb=5649890273cf8e660bba744e84ce5fee1e5efe69;p=helm.git

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a27b01831..9e0f85b58 100644
--- 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