diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index ad67becd0..1f6e99c7e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -11,7 +11,7 @@ *) open Pp -open Errors +open CErrors open Util open Names open Nameops |