new universes implementation

[helm.git] / helm / ocaml / tactics / tacticChaser.ml

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index f9c7feae7012589438ca3171d48d5e8407a4a6d1..c8217e78660b33a24a94f08a1fcdee6f18eb31f9 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -75,10 +75,10 @@ match list_of_must with
            if 
             let time = Unix.gettimeofday() in
             (try
-             ignore
+             ignore(ProofEngineTypes.apply_tactic 
                (PrimitiveTactics.apply_tac
                  ~term:(MQueryMisc.term_of_cic_textual_parser_uri
-                          (MQueryMisc.cic_textual_parser_uri_of_string uri))
+                          (MQueryMisc.cic_textual_parser_uri_of_string uri)))
                  status);
               let time1 = Unix.gettimeofday() in
                 prerr_endline (Printf.sprintf "%1.3f" (time1 -. time) );
@@ -179,9 +179,9 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
             try
               (m,
               (prerr_endline ("STO APPLICANDO " ^ uri);
-               (PrimitiveTactics.apply_tac
+               (ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac
                   ~term:(MQueryMisc.term_of_cic_textual_parser_uri
-                           (MQueryMisc.cic_textual_parser_uri_of_string uri))
+                           (MQueryMisc.cic_textual_parser_uri_of_string uri)))
                   status)))::tl'
             (* with ProofEngineTypes.Fail _ -> tl' *)
             (* patch to cover CSC's exportation bug *)