coqide menus on golas

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5104 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 44 insertions, 43 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 54a0e4736..cf54bfa2a 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -112,6 +112,7 @@ let interp s =
 	  | VernacDefinition _  | VernacStartTheoremProof _ 
 	  | VernacBeginSection _ | VernacGoal _
 	  | VernacDefineModule _ | VernacDeclareModuleType _
+	  | VernacDeclareTacticDefinition _
 		when is_in_proof_mode () -> 
 		  user_error_loc loc (str "CoqIDE do not support nested goals")
 	  | VernacDebug _ ->
@@ -277,7 +278,7 @@ let kwd = [(* "Compile";"Inductive";"Qed";"Type";"end";"Axiom";
   "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
   "CoInductive"; "Defined"; "Definition"; 
   "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
-  "Hints"; "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; 
+  "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; 
   "Infix"; "Lemma"; "Load"; "Local"; 
   "Match"; "Module"; "Module Type";
   "Mutual"; "Parameter"; "Print"; "Proof"; "Qed";
@@ -336,73 +337,73 @@ let reset_to_mod id =
 
 
 let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
-  [("Clear "^ident),("Clear "^ident^".");
+  [("clear "^ident),("clear "^ident^".");
    
-   ("Apply "^ident),
-   ("Apply "^ident^".");
+   ("apply "^ident),
+   ("apply "^ident^".");
    
-   ("Exact "^ident),
-   ("Exact "^ident^".");
+   ("exact "^ident),
+   ("exact "^ident^".");
 
-   ("Generalize "^ident),
-   ("Generalize "^ident^".");
+   ("generalize "^ident),
+   ("generalize "^ident^".");
    
-   ("Absurd <"^ident^">"),
-   ("Absurd "^
+   ("absurd <"^ident^">"),
+   ("absurd "^
     pr_ast
     ^".") ] @
 
    (if is_equation ast then
-      [ "Discriminate "^ident, "Discriminate "^ident^".";
-	"Injection "^ident, "Injection "^ident^"." ]
+      [ "discriminate "^ident, "discriminate "^ident^".";
+	"injection "^ident, "injection "^ident^"." ]
     else
       []) @
    
    (let _,t = splay_prod env sigma ast in
     if is_equation t then 
-      [ "Rewrite "^ident, "Rewrite "^ident^".";
-	"Rewrite <- "^ident, "Rewrite <- "^ident^"." ]
+      [ "rewrite "^ident, "rewrite "^ident^".";
+	"rewrite <- "^ident, "rewrite <- "^ident^"." ]
     else
       []) @
    
-  [("Elim "^ident),
-   ("Elim "^ident^".");
+  [("elim "^ident),
+   ("elim "^ident^".");
    
-   ("Inversion "^ident),
-   ("Inversion "^ident^".");
+   ("inversion "^ident),
+   ("inversion "^ident^".");
    
-   ("Inversion_clear "^ident),
-   ("Inversion_clear "^ident^".")] 
+   ("inversion clear "^ident),
+   ("inversion_clear "^ident^".")] 
 
 let concl_menu (_,_,concl,_) = 
   let is_eq = is_equation concl in
-  ["Intro", "Intro.";
-   "Intros", "Intros.";
-   "Intuition","Intuition." ] @
+  ["intro", "intro.";
+   "intros", "intros.";
+   "intuition","intuition." ] @
    
    (if is_eq then 
-      ["Reflexivity", "Reflexivity.";
-       "Discriminate", "Discriminate.";
-       "Symmetry", "Symmetry." ]
+      ["reflexivity", "reflexivity.";
+       "discriminate", "discriminate.";
+       "symmetry", "symmetry." ]
     else 
       []) @
 
-  ["Assumption" ,"Assumption.";
-   "Omega", "Omega.";
-   "Ring", "Ring.";
-   "Auto with *", "Auto with *.";
-   "EAuto with *", "EAuto with *.";
-   "Tauto", "Tauto.";
-   "Trivial", "Trivial.";
-   "Decide Equality", "Decide Equality.";
-
-   "Simpl", "Simpl.";
-   "Subst", "Subst.";
-
-   "Red", "Red.";
-   "Split", "Split.";
-   "Left", "Left.";
-   "Right", "Right.";
+  ["assumption" ,"assumption.";
+   "omega", "omega.";
+   "ring", "ring.";
+   "auto with *", "auto with *.";
+   "eauto with *", "eauto with *.";
+   "tauto", "tauto.";
+   "trivial", "trivial.";
+   "decide equality", "decide equality.";
+
+   "simpl", "simpl.";
+   "subst", "subst.";
+
+   "red", "red.";
+   "split", "split.";
+   "left", "left.";
+   "right", "right.";
   ]
 
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 890a38bf5..201f44c93 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -873,7 +873,7 @@ object(self)
 					   true
 					   true 
 					   false 
-					   (ip^"\n") 
+					   ("progress "^ip^"\n") 
 					   (ip^"\n"))
 				     )
 				  )