aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vernac_classifier.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/vernac_classifier.ml')
-rw-r--r--stm/vernac_classifier.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f6d8c327e..fa7acd00a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Vernacexpr
-open Errors
+open CErrors
open Pp
let default_proof_mode () = Proof_global.get_default_proof_mode_name ()