new universes implementation

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

diff --git a/helm/ocaml/tactics/statefulProofEngine.ml b/helm/ocaml/tactics/statefulProofEngine.ml
index 1c970249c78faed48ced7d1df0d7692d6cb7cf91..94710c412e034972ab65212f0497dd48098e7871 100644 (file)
--- a/helm/ocaml/tactics/statefulProofEngine.ml
+++ b/helm/ocaml/tactics/statefulProofEngine.ml
@@ -183,7 +183,7 @@ class ['a] status
       let old_internal_status = self#internal_status in
       let (new_proof, new_goals) =
         try
-          tactic (_proof, self#active_goal)
+          ProofEngineTypes.apply_tactic tactic (_proof, self#active_goal)
         with exn -> raise (Tactic_failure exn)
       in
       _proof <- new_proof;