From: Luca Padovani <luca.padovani@unito.it>
Date: Tue, 3 Jun 2003 08:49:32 +0000 (+0000)
Subject: * added mysterious function (Claudio can detail on it)
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=34320b90dd8eff0a3e14e2f15b8e3de59c49b9b4

* added mysterious function (Claudio can detail on it)
---

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index 6bef2dd43..b4b1f239a 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -89,7 +89,7 @@ let print_term ~ids_to_inner_sorts =
            X.xml_nempty "PROD" ["type",sort]
             [< List.fold_left
                 (fun i (id,binder,s) ->
-                  let sort = Hashtbl.find ids_to_inner_sorts id in
+                  let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
                    let attrs =
                     ("id",id)::("type",sort)::
                     match binder with
@@ -120,7 +120,6 @@ let print_term ~ids_to_inner_sorts =
             [< List.fold_left
                 (fun i (id,binder,s) ->
                   let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
-		  let _ = prerr_endline ("AHHHHHHHHHHHHHHHHH" ^ sort) in
                    let attrs =
                     ("id",id)::("type",sort)::
                     match binder with
diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 932771214..773050c56 100644
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -41,6 +41,8 @@ let fresh_id seed ids_to_terms ids_to_father_ids =
    res
 ;;
 
+let source_id_of_id id = "#source#" ^ id;;
+
 exception NotEnoughElements;;
 exception NameExpected;;
 
@@ -172,6 +174,9 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
                 aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
           | C.Lambda (n,s,t) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+	     let sourcetype = T.type_of_aux' metasenv context s in
+	      Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
+	       (string_of_sort sourcetype) ;
              if innersort = "Prop" then
               begin
                let father_is_lambda =
diff --git a/helm/gTopLevel/cic2acic.mli b/helm/gTopLevel/cic2acic.mli
index 0cd607bb6..b34d34342 100644
--- a/helm/gTopLevel/cic2acic.mli
+++ b/helm/gTopLevel/cic2acic.mli
@@ -26,6 +26,8 @@
 exception NotEnoughElements
 exception NameExpected
 
+val source_id_of_id : string -> string
+
 type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;