in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as

[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 3e9124e69bd2398c3eef1a02241d4154d1c607b7..b869536bf495cf5e3046a144be2bb39a1d983cde 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -496,6 +496,7 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
     | 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 (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
     | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~mk_choice ~env