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";