]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7fc80f3) | 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)
commita5ba8bfcd6ae3b5033e58792092924455cc51837
treec26ccd13f2fafcb3ff03adf70857ee005f418afetree | snapshot
parent7fc80f3be9d5d5d1d244abfe6fa5d27e57594878commit | 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 )
matita/library/logic/equality.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.