Uniformization of Coq tasks

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

1 files changed, 10 insertions, 9 deletions

diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index acc80cd62..7e47ca23f 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -6,18 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Coq
 
 class type ops =
 object
-  method go_to_insert : Coq.task
-  method tactic_wizard : string list -> Coq.task
-  method process_next_phrase : Coq.task
-  method process_until_end_or_error : Coq.task
-  method handle_reset_initial : Coq.reset_kind -> Coq.task
-  method raw_coq_query : string -> Coq.task
-  method show_goals : Coq.task
-  method backtrack_last_phrase : Coq.task
-  method initialize : Coq.task
+  method go_to_insert : unit task
+  method tactic_wizard : string list -> unit task
+  method process_next_phrase : unit task
+  method process_until_end_or_error : unit task
+  method handle_reset_initial : Coq.reset_kind -> unit task
+  method raw_coq_query : string -> unit task
+  method show_goals : unit task
+  method backtrack_last_phrase : unit task
+  method initialize : unit task
 end
 
 class coqops :