From 2f73b29c0ae7e4f0fa77934db55ebf811638fce3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 1 Jul 2003 15:25:38 +0000 Subject: [PATCH] - DoubleTypeInference.does_not_occur exposed - dummy bindings in Prods are no longer generated: arrows are now generated --- helm/gTopLevel/cic2acic.ml | 11 ++++++++++- helm/gTopLevel/doubleTypeInference.mli | 6 ++++++ 2 files changed, 16 insertions(+), 1 deletion(-) 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 -- 2.39.2