]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 10d3194) | patch
whd: ~delta=false now controls also zeta-reduction. This greatly speed-ups
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Mar 2008 13:25:42 +0000 (13:25 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Mar 2008 13:25:42 +0000 (13:25 +0000)
commitc036cf8b560ad40dbc06e94530af938e6f994aca
treee48c438a0688685176c15f10c110ec8bce620690tree | snapshot
parent10d3194c1b42dfa72e51000ff2cc217f937b43accommit | diff
whd: ~delta=false now controls also zeta-reduction. This greatly speed-ups
some operations when definitions are in the context.
Moreover, the semantics seems more reasonable (????).
helm/software/components/cic_proof_checking/cicReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.