From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Nov 2007 18:16:25 +0000 (+0000)
Subject: Bug fixed: local type declarations are not allowed in ocaml.
X-Git-Tag: 0.4.98@7921~17
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=0de121df33dac75fa7e5055b3a45e2b2fbeab1b1

Bug fixed: local type declarations are not allowed in ocaml.
---

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