From: Andrea Asperti Date: Tue, 23 Jan 2001 12:59:57 +0000 (+0000) Subject: - Bug due to overloading of csymbol letin fixed. X-Git-Tag: no-uwobo~14 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=138e51f3dc9bd6a42b84e45f9bf2c681cd411393;p=helm.git - 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. --- diff --git a/helm/style/content.xsl b/helm/style/content.xsl index a8d2ae856..65f982512 100644 --- a/helm/style/content.xsl +++ b/helm/style/content.xsl @@ -81,7 +81,7 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../] - letin + let_in diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 0d23a1837..24c4bdbe5 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -420,7 +420,7 @@ - + diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl index faf8d94ab..081711c53 100644 --- a/helm/style/proofs.xsl +++ b/helm/style/proofs.xsl @@ -97,10 +97,13 @@ - + + and count(child::*) = 6 + and name(*[5])='LAMBDA' + and name(*[5]/target/*[1])='LAMBDA'"> and_ind @@ -176,7 +179,10 @@