diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 1ea5025397..252b0967dc 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Pp open Names |