aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/rtauto
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto')
-rw-r--r--plugins/rtauto/proof_search.ml1
-rw-r--r--plugins/rtauto/refl_tauto.ml1
2 files changed, 2 insertions, 0 deletions
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index d773b1535..2448a2d39 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -7,6 +7,7 @@
(************************************************************************)
open Term
+open Errors
open Util
open Goptions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 4a9a0e47f..60ef81286 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -8,6 +8,7 @@
module Search = Explore.Make(Proof_search)
+open Errors
open Util
open Term
open Names