]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: afea2be) | patch
Some declarative tactics did not allow the "done" option in place
authormaiorino <??>
Tue, 3 Oct 2006 16:05:50 +0000 (16:05 +0000)
committermaiorino <??>
Tue, 3 Oct 2006 16:05:50 +0000 (16:05 +0000)
commite11e617809bbf3757ddfcbd6ef6d28d20e14a4f0
treecc7440f242e89b1ff04df2e06c80d6ff074229f3tree | snapshot
parentafea2be14c1c197e0804e8607fc6dcc49ce46955commit | diff
Some declarative tactics did not allow the "done" option in place
of "(id)". Fixed.
components/grafite/grafiteAst.ml diff | blob | history
components/grafite/grafiteAstPp.ml diff | blob | history
components/grafite_parser/grafiteParser.ml diff | blob | history
components/tactics/declarative.ml diff | blob | history
components/tactics/declarative.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.