diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-26 14:33:18 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-26 14:33:18 +0000 |
| commit | cde1310d3fe879b8f1c71118fa1cdd936560a64b (patch) | |
| tree | 28a37d9b7f590e8b289048b0bc9a86a56a1f9821 /checker/mod_checking.ml | |
| parent | 20ba5a3934067925fb08d6d464ebe5102d358d41 (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 'checker/mod_checking.ml')
0 files changed, 0 insertions, 0 deletions