aboutsummaryrefslogtreecommitdiff
path: root/plugins/dp
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/dp')
-rw-r--r--plugins/dp/dp.ml1
-rw-r--r--plugins/dp/dp_zenon.mll2
2 files changed, 2 insertions, 1 deletions
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 837195e44f..fd96b6d1c8 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -11,6 +11,7 @@
Zenon)
*)
+open Errors
open Util
open Pp
open Libobject
diff --git a/plugins/dp/dp_zenon.mll b/plugins/dp/dp_zenon.mll
index 949e91e344..1e82034c0c 100644
--- a/plugins/dp/dp_zenon.mll
+++ b/plugins/dp/dp_zenon.mll
@@ -3,7 +3,7 @@
open Lexing
open Pp
- open Util
+ open Errors
open Names
open Tacmach
open Dp_why