diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.mli | 1 | ||||
| -rw-r--r-- | interp/coqlib.mli | 1 | ||||
| -rw-r--r-- | interp/notation.mli | 2 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 1 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 2 | ||||
| -rw-r--r-- | interp/topconstr.mli | 1 |
6 files changed, 0 insertions, 8 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 868d53f33..161320626 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Util open Names open Libnames open Misctypes diff --git a/interp/coqlib.mli b/interp/coqlib.mli index a77b1060c..8146c4715 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -12,7 +12,6 @@ open Globnames open Nametab open Term open Pattern -open Errors open Util (** This module collects the global references, constructions and diff --git a/interp/notation.mli b/interp/notation.mli index 668d827f5..7629d86e7 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util open Pp open Bigint open Names diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 9dfc656a0..dee1203b3 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names open Notation_term open Misctypes diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index f0a45389a..d977a728d 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util open Names open Notation_term open Glob_term diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 482d409ba..bd9e776c9 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Errors open Names open Libnames open Glob_term |