X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2acic.ml;h=a3cdfbb78603d3237e3006fc5ecfb41543a279e5;hb=2f73b29c0ae7e4f0fa77934db55ebf811638fce3;hp=c18e7d6a684f7ba143a08cbebe12cd67fc59edbb;hpb=487bad7921f803801c4df83bf75c237927321fb1;p=helm.git

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index c18e7d6a6..a3cdfbb78 100644
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -172,8 +172,17 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
 	            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) ;
+              let n' =
+               match n with
+                  C.Anonymous -> n
+                | C.Name n' ->
+                   if D.does_not_occur 1 t then
+                    C.Anonymous
+                   else
+                    C.Name n'
+              in
                C.AProd
-                (fresh_id'', n, aux' context idrefs s,
+                (fresh_id'', n', aux' context idrefs s,
                  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 ;