From a8c20c4385d6045b848d21af9f30fc583de2aaa2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 5 Feb 2004 14:37:14 +0000 Subject: [PATCH] No longer puts anonymous declarations in the canonical contexts during eat_prods. --- helm/ocaml/cic_unification/cicRefine.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index c9c8f4d82..27929645b 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -502,7 +502,13 @@ and type_of_aux' metasenv context t = | Some t -> Some (CicMetaSubst.lift subst 1 t) ) args in let argty' = CicMetaSubst.lift subst (List.length args) argty in - let context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in + let name = + FreshNamesGenerator.mk_fresh_name + (CicMetaSubst.apply_subst_metasenv subst metasenv) + (CicMetaSubst.apply_subst_context subst context) + Cic.Anonymous + (CicMetaSubst.apply_subst subst argty) in + let context'' = Some (name, Cic.Decl argty') :: context' in let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv (context'' @ context) in let irl = @@ -511,14 +517,7 @@ and type_of_aux' metasenv context t = context) in let newmeta = Cic.Meta (idx, irl) in - let prod = - Cic.Prod - (FreshNamesGenerator.mk_fresh_name - (CicMetaSubst.apply_subst_metasenv subst metasenv) - (CicMetaSubst.apply_subst_context subst context) - Cic.Anonymous - (CicMetaSubst.apply_subst subst argty), - argty, newmeta) in + let prod = Cic.Prod (name, argty, newmeta) in let (_, subst, metasenv) = type_of_aux subst metasenv context prod in let (subst, metasenv) = CicUnification.fo_unif_subst subst context metasenv resty prod -- 2.39.2