diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/common.ml | 1 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 1 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 1 | ||||
| -rw-r--r-- | plugins/extraction/haskell.ml | 1 | ||||
| -rw-r--r-- | plugins/extraction/miniml.mli | 1 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.ml | 1 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.mli | 1 | ||||
| -rw-r--r-- | plugins/extraction/modutil.ml | 1 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 1 | ||||
| -rw-r--r-- | plugins/extraction/scheme.ml | 1 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 3 |
11 files changed, 12 insertions, 1 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 0bd5b84343..1b443f7535 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Names open Term diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 73062328b1..7c517dd9bc 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -11,6 +11,7 @@ open Declarations open Names open Libnames open Pp +open Errors open Util open Miniml open Table diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 219b3913fa..d9ee92c05e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open Errors open Util open Names open Term diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 96731ed27b..fe249cd65c 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -9,6 +9,7 @@ (*s Production of Haskell syntax. *) open Pp +open Errors open Util open Names open Nameops diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 5a19cc3f59..a5b57a4742 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -9,6 +9,7 @@ (*s Target language for extraction: a core ML called MiniML. *) open Pp +open Errors open Util open Names open Libnames diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index c244e046d3..f031709488 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -8,6 +8,7 @@ (*i*) open Pp +open Errors open Util open Names open Libnames diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 029e8cf468..630db6f069 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Names open Term diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 9e8dd8286c..123edd4c3f 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -10,6 +10,7 @@ open Names open Declarations open Environ open Libnames +open Errors open Util open Miniml open Table diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index ed69ec457b..d99bca6f4c 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -9,6 +9,7 @@ (*s Production of Ocaml syntax. *) open Pp +open Errors open Util open Names open Nameops diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 215076555a..157788ece9 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -9,6 +9,7 @@ (*s Production of Scheme syntax. *) open Pp +open Errors open Util open Names open Nameops diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 238befd256..6671824807 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -15,6 +15,7 @@ open Summary open Libobject open Goptions open Libnames +open Errors open Util open Pp open Miniml @@ -337,7 +338,7 @@ let warning_both_mod_and_cst q mp r = let error_axiom_scheme r i = err (str "The type scheme axiom " ++ spc () ++ - safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ + safe_pr_global r ++ spc () ++ str "needs " ++ int i ++ str " type variable(s).") let check_inside_module () = |