aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/evar_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/evar_tactics.ml')
-rw-r--r--ltac/evar_tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index 2e0996bf5..30aeba3bb 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Util
-open Errors
+open CErrors
open Evar_refiner
open Tacmach
open Tacexpr