From 4a2768c670a6904975fe6098c5bf7ea80ddb49e8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 23 Nov 2007 17:59:19 +0000 Subject: [PATCH] restored the right context used to generate names. see the comment --- helm/software/components/cic_unification/cicRefine.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index e4f4ef8e0..49c85a72e 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -166,7 +166,7 @@ let more_args_than_expected localization_tbl metasenv subst he context hetype' r enrich localization_tbl he ~f:(fun _-> msg) exn ;; -let mk_prod_of_metas metasenv context' subst args = +let mk_prod_of_metas metasenv context subst args = let rec mk_prod metasenv context' = function | [] -> let (metasenv, idx) = @@ -191,14 +191,11 @@ let mk_prod_of_metas metasenv context' subst args = (* then I generate a name --- using the hint name_hint *) (* --- that is fresh in context'. *) let name_hint = - (* Cic.Name "pippo" *) FreshNamesGenerator.mk_fresh_name ~subst metasenv - (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) - (CicMetaSubst.apply_subst_context subst context') + (CicMetaSubst.apply_subst_context subst context) Cic.Anonymous ~typ:(CicMetaSubst.apply_subst subst argty) in - (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) FreshNamesGenerator.mk_fresh_name ~subst [] context' name_hint ~typ:(Cic.Sort Cic.Prop) in @@ -207,7 +204,7 @@ let mk_prod_of_metas metasenv context' subst args = in metasenv,Cic.Prod (name,meta,target) in - mk_prod metasenv context' args + mk_prod metasenv context args ;; let rec type_of_constant uri ugraph = -- 2.39.2