]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 22ddac3) | patch
The tactic change is now working again. Moreover, it now receives a pattern
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Jun 2005 11:36:49 +0000 (11:36 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Jun 2005 11:36:49 +0000 (11:36 +0000)
commit21cb46a26fdff17b94e0a2e247bd144325f53f1e
tree2d30c73a84bdd7c0f50cac6982355f87fccf1479tree | snapshot
parent22ddac380a8574c0723b24f05c784d9a8690c736commit | diff
The tactic change is now working again. Moreover, it now receives a pattern
in input; moreover it handles correctly the with_what argument when it must
be put in a context different from the one it was parsed in.
helm/ocaml/tactics/primitiveTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.