From 97cc1d300867adfe4e0719997f9f534d8cea0fb8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 10 Nov 2007 14:07:13 +0000 Subject: [PATCH] a) Detection of existential types now implemented b) New heuristic for pretty printing of type definition arguments. --- helm/software/components/cic_exportation/cicExportation.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index e591a1278..75088e6fc 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/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 -- 2.39.2