X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2acic.ml;fp=helm%2FgTopLevel%2Fcic2acic.ml;h=773050c56fdee0ed556d1cf91d690995cc447512;hb=34320b90dd8eff0a3e14e2f15b8e3de59c49b9b4;hp=93277121428a9b7bc1346d817e9452ec191c6d5e;hpb=c313e16a5cc51ef7c4766aaafdf8f681eaf3d762;p=helm.git

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 =