From a066de71b5900198bc4f15c70421a525fa811276 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 24 May 2011 22:01:19 +0000 Subject: [PATCH] Quick patch to avoid name collisions when passing coercions under let...ins. --- matita/components/ng_refiner/nCicRefiner.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) 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), _ -> -- 2.39.2