diff options
Diffstat (limited to 'library/summary.ml')
| -rw-r--r-- | library/summary.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/summary.ml b/library/summary.ml index 697f57e8e..d2168540b 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util type 'a summary_declaration = { |