summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
94c7a26)
?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.
| NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
unify rdb test_eq_only metasenv subst context t2 t1 (not 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
| C.Meta (n,lc), t ->
instantiate rdb test_eq_only metasenv subst context n lc
(NCicReduction.head_beta_reduce ~subst t) swap