- DoubleTypeInference.does_not_occur exposed

[helm.git] / helm / gTopLevel / cic2acic.ml

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index c18e7d6a684f7ba143a08cbebe12cd67fc59edbb..a3cdfbb78603d3237e3006fc5ecfb41543a279e5 100644 (file)
--- 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 ;