]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9966e55) | patch
The two coercions sym_eq e eq_f gives BIG TROUBLES when checking composition during
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 9 Oct 2006 11:00:31 +0000 (11:00 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 9 Oct 2006 11:00:31 +0000 (11:00 +0000)
commit885eaebbb46c16f65ac312f6cf585700fc1b167d
tree9d1f66f14881cb306965f2ab70bf11f4f372745ftree | snapshot
parent9966e55f357cec5283b1b3d443178aeba68e065ecommit | diff
The two coercions sym_eq e eq_f gives BIG TROUBLES when checking composition during
qed. In particular, checking composition calls unification, that calls reductions,
that is problematic when there are a lot of lein in the context (as is it the case
with proofs generated by TPTP: see eg GRP486-1.p.ma )
helm/software/matita/library/logic/equality.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.