diff options
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."; |