diff options
Diffstat (limited to 'ide/coq_commands.ml')
| -rw-r--r-- | ide/coq_commands.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 36661cd2c..4a5e13db4 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -63,7 +63,7 @@ let commands = [ "Hint Unfold"; "Hypothesis";]; ["Identity Coercion"; - "Implicits"; + "Implicit Arguments"; "Inductive"; "Infix"; ]; @@ -196,6 +196,7 @@ let state_preserving = [ "Show"; "Show Conjectures"; + "Show Existentials"; "Show Implicits"; "Show Intro"; "Show Intros"; |