]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 252fbb5) | patch
First draft implementation of rewriting in an hypothesis.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 17 Nov 2005 16:15:29 +0000 (16:15 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 17 Nov 2005 16:15:29 +0000 (16:15 +0000)
commitdfbf84276e3183c190a6c7a59689324dccbaa6dc
tree23da549e419efb59d0f71eb294373d76945145eetree | snapshot
parent252fbb53c9d41d5d3f94bd9656adde26cd603ae3commit | diff
First draft implementation of rewriting in an hypothesis.
Highly incomplete. Fails randomly if the pattern is not one the tactic is able
to cope with.
helm/matita/tests/rewrite.ma diff | blob | history
helm/ocaml/tactics/equalityTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.