From 86ff79af764c2a434fdf38ea344ab722811981c8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Apr 2009 15:50:28 +0000 Subject: [PATCH] eta-contraction was made on the wrong term --- helm/software/components/ng_refiner/nCicUnification.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index d64fb005f..006fcafe1 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -317,11 +317,11 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = (C.Meta (i,l)) lambda_Mj in let t1 = NCicReduction.whd ~subst context t1 in - let i, l = + let j, lj = match t1 with NCic.Meta (i,l) -> i, l | _ -> assert false in let metasenv, subst = - instantiate hdb test_eq_only metasenv subst context i l t2 true + instantiate hdb test_eq_only metasenv subst context j lj t2 true in (try let name, ctx, term, ty = NCicUtils.lookup_subst i subst in -- 2.39.2