From 0de121df33dac75fa7e5055b3a45e2b2fbeab1b1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Nov 2007 18:16:25 +0000 Subject: [PATCH] Bug fixed: local type declarations are not allowed in ocaml. --- components/cic_exportation/cicExportation.ml | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml index 8af058f96..58e817091 100644 --- a/components/cic_exportation/cicExportation.ml +++ b/components/cic_exportation/cicExportation.ml @@ -183,9 +183,19 @@ let rec pp ~in_type t context = "(function " ^ ppname b ^ " -> " ^ pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")") | C.LetIn (b,s,t) -> - 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) ^ ")" + (match analyze_term context s with + `Type + | `Proof -> + let ty,_ = + CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph + in + pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) + | `Term -> + 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 -- 2.39.2