X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=508411d2847b1b84083141efa5bbe14aed16a8fa;hb=9b09890767aaa93e512324f8e7f13e2cdeebac88;hp=61e77c6fe12047b9efbe5939a362df8b088333fb;hpb=430d6307ae5776ed000a78358a2881cb88936c37;p=helm.git

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index 61e77c6fe..508411d28 100644
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -109,7 +109,7 @@ let ast_of_acic0 ~output_type term_info acic k =
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type _ -> `Pi
+          | `Set | `Type _ | `NType _ -> `Pi
           | `Prop | `CProp _ -> `Forall
         in
         idref id (Ast.Binder (binder_kind,