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

[helm.git] / helm / software / components / acic_content / termAcicContent.ml

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index fb890915298b5bb70846c1cc01e1337e56c3ba5f..c02c5892d65aa62583d0dc0a1bd93c6a8184ff22 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -126,7 +126,7 @@ let ast_of_acic0 ~output_type term_info acic k =
         let binder_kind =
           match sort_of_id id with
           | `Set | `Type _ | `NType _ -> `Pi
-          | `Prop | `CProp _ -> `Forall
+          | `Prop | `CProp _ | `NCProp _ -> `Forall
         in
         idref id (Ast.Binder (binder_kind,
           (CicNotationUtil.name_of_cic_name n, Some (k s)), k t))