]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a6f4d10) | patch
In order to prevent useless meta extensions, we optimize the unification of one
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 24 Nov 2009 16:42:01 +0000 (16:42 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Tue, 24 Nov 2009 16:42:01 +0000 (16:42 +0000)
commit3f14041310efe95e436bea8efd51ebdab67d5def
tree79dbf905840fe70d0a0ceb826f9b41bb475d297btree | snapshot
parenta6f4d10cfad6b1ba9c9e32b2d095346ab5f7aa3fcommit | diff
In order to prevent useless meta extensions, we optimize the unification of one
type and one unrefined term (currently happening only in the Lambda case).
helm/software/components/ng_refiner/nCicRefiner.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.