]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bf07cdb) | patch
Bug fixed: metavariables generated by the saturation in the rewrite tactic
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 Jul 2005 10:21:29 +0000 (10:21 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 Jul 2005 10:21:29 +0000 (10:21 +0000)
commit016e4c6fc449b50ac19e73eb952cfb2dc64f4398
tree91a653dd977bb6985a73a43195acd889566ec996tree | snapshot
parentbf07cdb635f9a3eb858a1b7980f848f3e40a439ccommit | diff
Bug fixed: metavariables generated by the saturation in the rewrite tactic
were not declared as new goals in the output of the tactic.
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.