]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2289472) | patch
Unfold tactic generalized to perform zeta-reduction.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Sep 2005 16:48:46 +0000 (16:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Sep 2005 16:48:46 +0000 (16:48 +0000)
commit8bbe4f30e98b4a1e0d51d17b64905461df669101
treebfebe1ff5e4fcdb6dca309289e0280db4dc0899btree | snapshot
parent2289472271cf56d3af77fbbe634b643eac474a13commit | diff
Unfold tactic generalized to perform zeta-reduction.
WARNING: the tactic is bugged since it tries to zeta-expand a term that lives
in the context of the goal, not in the context of the pattern!
helm/ocaml/tactics/proofEngineReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.