From a6f4d10cfad6b1ba9c9e32b2d095346ab5f7aa3f Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 24 Nov 2009 15:46:34 +0000 Subject: [PATCH] When unifying ?1[a,b] == ?2[a,b,c] it is not the same to instantiate ?1 or ?2: instantiating ?2 may drop the dependency over c, while instatianting ?1 does no harm. This patch always instantiates the meta whose canonical context is a prefix, or the newest one if the two canonical contexts are the same. --- helm/software/components/ng_refiner/nCicUnification.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 805ea859f..466c0ef85 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -546,6 +546,15 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst -> unify rdb test_eq_only metasenv subst context t2 t1 (not swap) + | C.Meta (n,_), C.Meta (m,lc') when + let _,cc1,_ = NCicUtils.lookup_meta n metasenv in + let _,cc2,_ = NCicUtils.lookup_meta m metasenv in + (n < m && cc1 = cc2) || + let len1 = List.length cc1 in + let len2 = List.length cc2 in + len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) -> + instantiate rdb test_eq_only metasenv subst context m lc' + (NCicReduction.head_beta_reduce ~subst t1) (not swap) | C.Meta (n,lc), t -> instantiate rdb test_eq_only metasenv subst context n lc (NCicReduction.head_beta_reduce ~subst t) swap -- 2.39.2