]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cfa0c77) | patch
new case for higher order unification:
authorEnrico Tassi <enrico.tassi@inria.fr>
Sun, 17 Oct 2010 09:08:05 +0000 (09:08 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sun, 17 Oct 2010 09:08:05 +0000 (09:08 +0000)
commit3b4ec24b0bf7b1cd23cdc632fa3fcbb9dbbda139
tree8a312c54e505065355a02e9fed35a6721cafb813tree | snapshot
parentcfa0c7797b5c96c49c9f0cf7b5fd1ccae9889766commit | diff
new case for higher order unification:

  (? ?) =?= (f x)

is not handled by delift, since flexible arguments in the local context
are skipped by delift, resulting in the instantiation of the head meta to
a constant function, even if the rhs is structurally the same.
helm/software/components/ng_refiner/nCicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.