fixed groebner as a plugin + pattern matching Timeout

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

6 files changed, 10 insertions, 3 deletions

diff --git a/Makefile.build b/Makefile.build
index 5513c854a0..508b007c57 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -943,7 +943,7 @@ endif
 	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c $<
 
 %.cmxs: %.cmxa
-	$(SHOW)'OCAMLOPT  $<'
+	$(SHOW)'OCAMLOPT -shared -o $@'
 ifneq ($(HASNATDYNLINK),os5fixme)
 	$(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
 else
@@ -965,7 +965,7 @@ else
 endif
 
 %.cmxs: %.cmx
-	$(SHOW)'OCAMLOPT  $<'
+	$(SHOW)'OCAMLOPT -shared -o $@'
 	$(HIDE)$(OCAMLOPT) -shared -o $@ $<
 
 %.ml: %.mll
diff --git a/contrib/groebner/GroebnerR.v b/contrib/groebner/GroebnerR.v
index c64bc88159..5f6d35d8a5 100644
--- a/contrib/groebner/GroebnerR.v
+++ b/contrib/groebner/GroebnerR.v
@@ -40,7 +40,7 @@ Require Import BinPos.
 Require Import BinList.
 Require Import InitialRing.
 
-Declare ML Module "groebner".
+Declare ML Module "groebner_plugin".
 
 Open Scope R_scope.
 
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index c2035586fb..f0b68fb7c1 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -195,6 +195,7 @@ and ct_COMMAND =
   | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT
   | CT_time of ct_COMMAND
+  | CT_timeout of ct_INT * ct_COMMAND
   | CT_undo of ct_INT_OPT
   | CT_unfocus
   | CT_unset_option of ct_TABLE
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index b9daf63574..1714440dfb 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -617,6 +617,10 @@ and fCOMMAND = function
 | CT_time(x1) ->
    fCOMMAND x1 ++
    fNODE "time" 1
+| CT_timeout(n,x1) ->
+    fINT n ++
+    fCOMMAND x1 ++
+    fNODE "timeout" 2
 | CT_undo(x1) ->
    fINT_OPT x1 ++
    fNODE "undo" 1
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c8684a9a0e..64a9b5c8c0 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -2192,6 +2192,7 @@ let rec xlate_vernac =
   | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
   | VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s)
   | VernacTime(v) -> CT_time(xlate_vernac v)
+  | VernacTimeout(n,v) -> CT_timeout(CT_int n,xlate_vernac v)
   | VernacSetOption (Goptions.SecondaryTable ("Implicit", "Arguments"), BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
   |VernacExactProof f -> CT_proof(xlate_formula f)
   | VernacSetOption (table, BoolValue true) -> 
diff --git a/ide/coq.ml b/ide/coq.ml
index 47fae64eaa..ff75b6c177 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -194,6 +194,7 @@ type command_attribute =
 let rec attribute_of_vernac_command = function
   (* Control *)
   | VernacTime com -> attribute_of_vernac_command com
+  | VernacTimeout(_,com) -> attribute_of_vernac_command com
   | VernacList _ -> [] (* unsupported *)
   | VernacLoad _ -> []