]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fd08bfe) | patch
procedural: added fwd rewrite in arbitrary proofs (not just premises)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 12 Jan 2007 19:34:58 +0000 (19:34 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 12 Jan 2007 19:34:58 +0000 (19:34 +0000)
commitad45ff0a9bc4ddbfe0691ce1edbfa8784b37aa8e
tree3a2eca901bcc3f12cd6f8e12d4b2bf77c68f2e3btree | snapshot
parentfd08bfeab5fc4c01a1716b9c3fe95ed8439c5190commit | diff
procedural: added fwd rewrite in arbitrary proofs (not just premises)
            added whd conversion before intros when needed
prova.ma  : highlighted a bug with the "in" clause of the "match" constr.
components/content_pres/.depend diff | blob | history
components/content_pres/.depend.opt diff | blob | history
components/content_pres/Makefile diff | blob | history
components/content_pres/acic2Procedural.ml diff | blob | history
components/content_pres/proceduralConversion.ml [new file with mode: 0644] blob
components/content_pres/proceduralConversion.mli [new file with mode: 0644] blob
components/content_pres/proceduralTypes.ml diff | blob | history
components/content_pres/proceduralTypes.mli diff | blob | history
matita/contribs/prova.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.