From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 24 May 2011 22:01:19 +0000 (+0000)
Subject: Quick patch to avoid name collisions when passing coercions under let...ins.
X-Git-Tag: make_still_working~2490
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a066de71b5900198bc4f15c70421a525fa811276;p=helm.git

Quick patch to avoid name collisions when passing coercions under let...ins.
---

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index e0f920fff..05d7a0fa8 100644
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -804,14 +804,20 @@ and try_coercions status
         in
         metasenv, subst, t, expty (*}}}*)
     | _,_,NCic.LetIn(name,ty,t,bo) -> 
+        let rec mk_fresh_name ctx firstch n =
+          let candidate = (String.make 1 firstch) ^ (string_of_int n) in
+          if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
+          else mk_fresh_name ctx firstch (n+1)
+        in
         pp (lazy "LETIN");
-        let context_bo = (name, NCic.Def (t,ty)) :: context in
+        let name' = mk_fresh_name context 'l' 0 in
+        let context_bo = (name', NCic.Def (t,ty)) :: context in
         let metasenv, subst, bo2, _ = 
           try_coercions status ~localise metasenv subst context_bo
            bo orig_t (NCicSubstitution.lift status 1 infty)
            (NCicSubstitution.lift status 1 expty) perform_unification exc
         in
-        let coerced = NCic.LetIn (name,ty,t,bo2) in
+        let coerced = NCic.LetIn (name',ty,t,bo2) in
         pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
         metasenv, subst, coerced, expty
     | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ ->