From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 1 Jul 2003 15:25:38 +0000 (+0000)
Subject: - DoubleTypeInference.does_not_occur exposed
X-Git-Tag: camera_ready~27
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2f73b29c0ae7e4f0fa77934db55ebf811638fce3

- 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 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 ;
diff --git a/helm/gTopLevel/doubleTypeInference.mli b/helm/gTopLevel/doubleTypeInference.mli
index aa151988b..d7d06ae42 100644
--- 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