aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eqschemes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/eqschemes.ml')
-rw-r--r--tactics/eqschemes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index a03489c80..1a45217a4 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -44,7 +44,7 @@
natural expectation of the user.
*)
-open Errors
+open CErrors
open Util
open Names
open Term