aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.stage3
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-26 14:33:18 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-26 14:33:18 +0000
commitcde1310d3fe879b8f1c71118fa1cdd936560a64b (patch)
tree28a37d9b7f590e8b289048b0bc9a86a56a1f9821 /Makefile.stage3
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 'Makefile.stage3')
0 files changed, 0 insertions, 0 deletions