From 2bfd692efc9b2c41d67d31bf36801d150f5715fc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 28 Dec 2006 17:12:06 +0000 Subject: [PATCH] Yet another localization error in eat_prods fixed. However, the fix is very very ugly (it uses unsharing) and clearly shows a source of inefficiency (and possibly also divergence, I would say). --- helm/software/components/cic_unification/cicRefine.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 4fc9f4ccc..95651c49f 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -1332,7 +1332,12 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il he in let x,xty,subst,metasenv,ugraph = - type_of_aux subst metasenv context x ugraph + (*CSC: here unsharing is necessary to avoid an unwanted + relocalization. However, this also shows a great source of + inefficiency: "x" is refined twice (once now and once in the + subsequent eat_prods_and_args). Morevoer, how is divergence avoided? + *) + type_of_aux subst metasenv context (Unshare.unshare x) ugraph in let carr_src = CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) -- 2.39.2