]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0d750a8) | patch
elim_tac rewritten almost entirely. It is now based on refinement +
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 18 Jun 2004 11:29:22 +0000 (11:29 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 18 Jun 2004 11:29:22 +0000 (11:29 +0000)
commit2697b6b76d4a2449ac9ad6657128c0cc3d90ac65
tree857905d0603f4225422e95c6b500c0f545539bcatree | snapshot
parent0d750a87e8b3f26964fc5a05cf559d86c913d962commit | diff
elim_tac rewritten almost entirely. It is now based on refinement +
one invocation of the (now more powerful than before) apply_tac.
helm/ocaml/tactics/primitiveTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.