From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Tue, 24 Nov 2009 15:46:34 +0000 (+0000)
Subject: When unifying
X-Git-Tag: make_still_working~3199
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a6f4d10cfad6b1ba9c9e32b2d095346ab5f7aa3f;hp=94c7a260ca00f045a3ec1b371f19de757f83003b;p=helm.git

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

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