- DoubleTypeInference.does_not_occur exposed

- dummy bindings in Prods are no longer generated: arrows are now generated

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 ;

diff --git a/helm/gTopLevel/doubleTypeInference.mli b/helm/gTopLevel/doubleTypeInference.mli
index aa151988b233875ab4721aa3106b2189a73bd778..d7d06ae42346f96eb3cb89ab0128597b7d0e4d5e 100644 (file)
--- a/helm/gTopLevel/doubleTypeInference.mli
+++ b/helm/gTopLevel/doubleTypeInference.mli
@@ -17,3 +17,9 @@ module CicHash :
 
 val double_type_of :
  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term option -> types CicHash.t
+
+(** Auxiliary functions **)
+
+(* does_not_occur n te                              *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+val does_not_occur : int -> Cic.term -> bool