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 805ea859f8beef8be33eb03d123b850f37a5c48e..466c0ef855bf93b0bbd4a84ac06eee43558d8fde 100644 (file)
--- 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