From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 28 Dec 2006 17:12:06 +0000 (+0000)
Subject: Yet another localization error in eat_prods fixed.
X-Git-Tag: make_still_working~6562
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2bfd692efc9b2c41d67d31bf36801d150f5715fc;p=helm.git

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).
---

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)