]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 38d63e5) | patch
some improvements in the anticipator
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 6 Feb 2015 19:40:26 +0000 (19:40 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 6 Feb 2015 19:40:26 +0000 (19:40 +0000)
commit24b593925bae7964bdc61e28408d389e5a74bd7a
tree879e42a7d879bbf5cb084ecddc13e1a343eabbe3tree | snapshot
parent38d63e5adf7f0eeeab575697e10c2867cc1c2a7fcommit | diff
some improvements in the anticipator
- we anticipate the terms to be matched
- we do not anticipate inner fixpoints because we turn them into constants when we generate Grafite for the ng_kernel
matita/matita/contribs/lambdadelta/basic_1/lift/defs.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_1/lift/fwd.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_1/lift/props.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_1/lift/tlt.ma diff | blob | history
matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.