diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.mli | 1 | ||||
| -rw-r--r-- | pretyping/coercion.mli | 1 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 1 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 2 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 2 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 2 | ||||
| -rw-r--r-- | pretyping/typeclasses_errors.mli | 1 |
9 files changed, 0 insertions, 13 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index d0dd870de0..7add91c161 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Pp open Names open Term diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 45566e9fbc..b2e41841ee 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Pp open Evd open Names diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 82d154d399..ea0f063fe4 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Pp open Util open Names diff --git a/pretyping/evd.mli b/pretyping/evd.mli index ca552a450b..70a18b54af 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -7,8 +7,6 @@ (************************************************************************) open Pp -open Errors -open Util open Names open Term open Sign diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 19d003a92c..6a26fe1d43 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Pp -open Util open Names open Sign open Term diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 7debe2b0d1..2410fb7ca2 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -7,8 +7,6 @@ (************************************************************************) open Pp -open Errors -open Util open Names open Term open Sign diff --git a/pretyping/termops.mli b/pretyping/termops.mli index e5dc2448bc..d2141c50ed 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Util open Pp open Names diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 6c97516cad..411651afe5 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -16,8 +16,6 @@ open Environ open Nametab open Mod_subst open Topconstr -open Errors -open Util type direction = Forward | Backward diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 925222766a..a05258de75 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -15,7 +15,6 @@ open Environ open Nametab open Mod_subst open Constrexpr -open Errors open Pp open Globnames |