aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authormsozeau2008-10-26 14:33:18 +0000
committermsozeau2008-10-26 14:33:18 +0000
commitcde1310d3fe879b8f1c71118fa1cdd936560a64b (patch)
tree28a37d9b7f590e8b289048b0bc9a86a56a1f9821 /dev/base_include
parent20ba5a3934067925fb08d6d464ebe5102d358d41 (diff)
Stop using a coqdocdoc env which prevents use of environments inside
comments that go across code and doc (e.g. for beamer frames), it was unused anyway. Add "do" and "repeat" as tactic identifiers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11507 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions