aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
diff options
context:
space:
mode:
authorMaxime Dénès2016-07-03 18:54:06 +0200
committerMaxime Dénès2016-07-03 18:54:06 +0200
commite278d031a1d9a7bf3de463d3d415065299c99395 (patch)
treeddd3a123e1887a9fa4634af7559bc7bb67b0cc25 /printing/ppvernac.ml
parentd7664c0530edd196d52e9fd8a4b925dbfefd1b9b (diff)
parent3ce70f21a18cc19e720e8ac54b93652527881942 (diff)
Merge branch 'cerrors-cclosure' into trunk
Was PR#226: CErrors & CClosure
Diffstat (limited to 'printing/ppvernac.ml')
-rw-r--r--printing/ppvernac.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5b73b054dd..0d47b34dfd 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -9,7 +9,7 @@
open Pp
open Names
-open Errors
+open CErrors
open Util
open Extend
open Vernacexpr
@@ -1082,7 +1082,7 @@ module Make
)
| VernacSetOpacity _ ->
return (
- Errors.anomaly (keyword "VernacSetOpacity used to set something else")
+ CErrors.anomaly (keyword "VernacSetOpacity used to set something else")
)
| VernacSetStrategy l ->
let pr_lev = function
@@ -1219,7 +1219,7 @@ module Make
let pr_vernac v =
try pr_vernac_body v ++ sep_end v
- with e -> Errors.print e
+ with e -> CErrors.print e
end