From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 10 Nov 2007 14:07:13 +0000 (+0000)
Subject: a) Detection of existential types now implemented
X-Git-Tag: 0.4.95@7852~27
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b2abc81f0b76224f6f4f526feaf1fefd6178ae7d;p=helm.git

a) Detection of existential types now implemented
b) New heuristic for pretty printing of type definition arguments.
---

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index e591a1278..75088e6fc 100644
--- a/components/cic_exportation/cicExportation.ml
+++ b/components/cic_exportation/cicExportation.ml
@@ -186,6 +186,10 @@ let rec pp ~in_type t context =
        let ty,_ = CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph in
        "(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^
         pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
+    | C.Appl (he::tl) when in_type ->
+       let hes = pp ~in_type he context in
+       let stl = String.concat "," (clean_args_for_ty context tl) in
+        (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
     | C.Appl (C.MutInd _ as he::tl) ->
        let hes = pp ~in_type he context in
        let stl = String.concat "," (clean_args_for_ty context tl) in
@@ -410,6 +414,9 @@ let ppty current_module_uri =
              let abstr,args =
               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
                abstr,pp ~in_type:true current_module_uri s context::args
+         | `Sort _ when nparams <= 0 ->
+             let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
+              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
          | `Sort _ ->
              let n =
               match n with