]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ec4278c) | patch
- Bug due to overloading of csymbol letin fixed.
authorAndrea Asperti <andrea.asperti@unibo.it>
Tue, 23 Jan 2001 12:59:57 +0000 (12:59 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Tue, 23 Jan 2001 12:59:57 +0000 (12:59 +0000)
commit138e51f3dc9bd6a42b84e45f9bf2c681cd411393
treef46636b598182e750aee6fc4a69b649115ae6700tree | snapshot
parentec4278cb76dd6238be23a8883cd85f152d7c1ac7commit | diff
- Bug due to overloading of csymbol letin fixed.
Now we have both let_in (for CIC LETIN) and letin (generated
by proof transformation).

- Bug of apply_ind fixed. If the proof of A->B->C is not of
the form \x.\y.M, than no special treatment is done.
helm/style/content.xsl diff | blob | history
helm/style/mmlextension.xsl diff | blob | history
helm/style/proofs.xsl diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.