diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-16 19:17:27 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-16 19:17:27 +0000 |
commit | b9e27721e88872a93ec7ca91575304ce1496a0ef (patch) | |
tree | 355b6e71179b8ace71691c22033874f6e7b6cae9 /ide/coq_commands.ml | |
parent | 481494be9f20d9c497e4d7ac108ae19bbaa53201 (diff) |
Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9656 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq_commands.ml')
-rw-r--r-- | ide/coq_commands.ml | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 4dde60111..a8edc4061 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -77,10 +77,17 @@ let commands = [ ["Module"; "Module Type"; "Mutual Inductive";]; - ["Notation";]; - ["Opaque";]; + ["Notation"; + "Next Obligation";]; + ["Opaque"; + "Obligations Tactic";]; ["Parameter"; - "Proof."]; + "Proof."; + "Program Definition"; + "Program Fixpoint"; + "Program Lemma"; + "Program Theorem"; + ]; ["Qed."; ]; ["Read Module"; @@ -155,6 +162,8 @@ let state_preserving = [ "Extraction Module"; "Inspect"; "Locate"; + + "Obligations"; "Print"; "Print All."; "Print Classes"; |