From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Sat, 18 Aug 2007 20:34:57 +0000
Subject: Imported Upstream version 8.1.pl1+dfsg

---
 ide/coq_commands.ml | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

(limited to 'ide/coq_commands.ml')

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 30d99f5b..677c5eff 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_commands.ml 7102 2005-06-03 13:14:27Z coq $ *)
+(* $Id: coq_commands.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
 
 let commands = [
   [(* "Abort"; *)
@@ -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";
-- 
cgit v1.2.3