X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=68afd810b6c8f3c0c0aa1d4222dc391602aaafc9;hb=190c0efe22d097c4b4e85207342224622b1fccb9;hp=41c24c9ae5a11065df8c8ccc9e5c632911c60cac;hpb=d005e7130f74df3db81828c0fe7f3439a25d5002;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 41c24c9ae..68afd810b 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -542,7 +542,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
-    | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
     | _ -> assert false (* god bless Bologna *)