]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7ae585c) | patch
Bug fixed in generalization: the goals opened by lazy parsing of the
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 1 Feb 2006 18:35:29 +0000 (18:35 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 1 Feb 2006 18:35:29 +0000 (18:35 +0000)
commitf345c59c259bc72379996c951561a0aa3ca06dc9
tree94b0686abbfec0fb4b927a26d4910f772e3fcdb5tree | snapshot
parent7ae585c99c2e9d9b7c9c100b11a18c220bfbd4e8commit | diff
Bug fixed in generalization: the goals opened by lazy parsing of the
generalization argument were not reported correctly. This fix is not
100% correct, but it will do for now. The best solution would be to
add a new tactic to modify the metasenv and to make the status type
private.
helm/ocaml/tactics/variousTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.