aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq_commands.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq_commands.ml')
-rw-r--r--ide/coq_commands.ml9
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.";