]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 94c7a26) | patch
When unifying
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 24 Nov 2009 15:46:34 +0000 (15:46 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 24 Nov 2009 15:46:34 +0000 (15:46 +0000)
commita6f4d10cfad6b1ba9c9e32b2d095346ab5f7aa3f
treea1eb25fa123b0c847d131b8378b0141773c262eatree | snapshot
parent94c7a260ca00f045a3ec1b371f19de757f83003bcommit | diff
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 diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.