diff options
| author |  marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-12 14:12:22 +0000 |
|---|---|---|
| committer | marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-12 14:12:22 +0000 |
| commit | e653960a72cbf0bd95e7cef97cd9000eb44fd267 (patch) | |
| tree | 061ac7e6d97ae753a63f217adefadb0a78732ebd /ide/coq_commands.ml | |
| parent | 0347ba1eecdbc803e2f960074c4fd63a39c8f698 (diff) | |
plus de syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5089 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq_commands.ml')
| -rw-r--r-- | ide/coq_commands.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index aefae8fbb..7173bfc2f 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -60,12 +60,11 @@ let commands = [ "Grammar";]; ["Hint"; "Hint Constructors"; - "Hint Unfold"; + "Hint Extern"; + "Hint Immediate"; + "Hint Resolve"; "Hint Rewrite"; - "Hints Extern"; - "Hints Immediate"; - "Hints Resolve"; - "Hints Unfold"; + "Hint Unfold"; "Hypothesis";]; ["Identity Coercion"; "Implicit Arguments Off."; |