X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=ed28894a7f6320c0f326c5b3fbf3ce07c911c2e6;hb=d3f1cdd3ebec515770d4c2f8a4f7bbc1859e8946;hp=2b469ce9d7d4b24585421f5007ff1cc80602c1f4;hpb=93ce01455cfeba6b29e3c8a57e28f56559fb891d;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 2b469ce9d..ed28894a7 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -484,11 +484,15 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
     | 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 (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
     | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~mk_choice ~env
          (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
-    | _ -> assert false (* god bless Bologna *)
+    | CicNotationPt.Variable _
+    | CicNotationPt.Magic _
+    | CicNotationPt.Layout _
+    | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
   and aux_option ~localize loc context annotation = function
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term