diff options
Diffstat (limited to 'pretyping')
31 files changed, 0 insertions, 71 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9809d4d09..b5bb27da9 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open Context diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 58265208b..886e00e83 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -18,7 +18,6 @@ open Environ open Libobject open Term open Termops -open Decl_kinds open Mod_subst (* usage qque peu general: utilise aussi dans record *) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index d0c7793ae..7bde9e910 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -7,11 +7,9 @@ (************************************************************************) open Names -open Decl_kinds open Term open Evd open Environ -open Nametab open Mod_subst (** {6 This is the type of class kinds } *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index f5c548cc4..c1b114c91 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -6,13 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Evd open Names open Term -open Context open Environ -open Evarutil open Glob_term (** {6 Coercions. } *) diff --git a/pretyping/constrMatching.mli b/pretyping/constrMatching.mli index b82f11525..19cf34877 100644 --- a/pretyping/constrMatching.mli +++ b/pretyping/constrMatching.mli @@ -12,7 +12,6 @@ open Names open Term open Environ open Pattern -open Termops (** [PatternMatchingFailure] is the exception raised when pattern matching fails *) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 8a10b7ed5..2cca25fd2 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Pp open Names open Term open Context diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 89993189f..3a8e4fab5 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -8,9 +8,7 @@ open Names open Term -open Context open Environ -open Termops open Reductionops open Evd open Locus diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 20a4a3f9e..bdc4bc0ae 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Util open Errors open Names diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f4636cdaa..49ce29fdf 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -20,7 +20,6 @@ open Environ open Evd open Reductionops open Pretype_errors -open Retyping (****************************************************) (* Expanding/testing/exposing existential variables *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7e1f7df88..f41f1ec86 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,15 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Util open Names -open Glob_term open Term open Context open Evd open Environ -open Reductionops (** {5 This modules provides useful functions for unification modulo evars } *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 2b0e9ca68..8f423c788 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -8,14 +8,11 @@ open Util open Loc -open Pp open Names open Term open Context open Environ -open Libnames open Mod_subst -open Termops (** {5 Existential variables and unification states} diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 1785c87be..9e0aac909 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -6,15 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names -open Context -open Term -open Libnames -open Nametab -open Decl_kinds -open Misctypes -open Locus open Glob_term (** Equalities *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 610a7bf39..6bcfac20e 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -8,8 +8,6 @@ open Names open Term -open Declarations -open Inductiveops open Environ open Evd diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index ddf615033..a086a6f58 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Misctypes open Locus (** Utilities on occurrences *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index cc2054d10..af7a99320 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -16,10 +16,7 @@ open Declarations open Names open Inductive open Util -open Unix open Nativecode -open Inductiveops -open Closure open Nativevalues open Nativelambda diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index a589846b9..8f65ddb2f 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -5,10 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Environ -open Reduction open Evd open Nativelambda diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 5cc4049ba..cfe71510a 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -6,13 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Names open Context open Term -open Environ open Globnames -open Nametab open Glob_term open Mod_subst open Misctypes diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 404f5b401..8ffd53055 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -9,9 +9,6 @@ open Util open Names open Term -open Vars -open Termops -open Namegen open Environ open Type_errors diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 996b75146..8e98f6307 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -6,13 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term -open Context open Environ -open Glob_term -open Inductiveops open Type_errors (** {6 The type of errors raised by the pretyper } *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 6994723ac..ec8aae140 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -13,7 +13,6 @@ implicit arguments. *) open Names -open Context open Term open Environ open Evd diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 88199c434..42663c014 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -7,10 +7,8 @@ (************************************************************************) open Names -open Nametab open Term open Globnames -open Libobject (** Operations concerning records and canonical structures *) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index aff65d53a..5ba0d74ec 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -12,7 +12,6 @@ open Context open Univ open Evd open Environ -open Closure (** Reduction Functions. *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 963d61ca2..bb3ffa411 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Evd open Environ diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 4b03c935f..dd7542fc7 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -16,7 +16,6 @@ open Libnames open Globnames open Termops open Namegen -open Libobject open Environ open Closure open Reductionops diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index be92be51a..34aca3e33 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -11,9 +11,6 @@ open Term open Environ open Evd open Reductionops -open Closure -open Glob_term -open Termops open Pattern open Globnames open Locus diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli index 2560ae080..7825ebdf1 100644 --- a/pretyping/term_dnet.mli +++ b/pretyping/term_dnet.mli @@ -7,8 +7,6 @@ (************************************************************************) open Term -open Context -open Libnames open Mod_subst (** Dnets on constr terms. diff --git a/pretyping/termops.mli b/pretyping/termops.mli index d9213fc13..d0d3fd767 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Pp open Names open Term diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 0fe22bcce..c36293525 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -8,14 +8,10 @@ open Names open Globnames -open Decl_kinds open Term open Context open Evd open Environ -open Nametab -open Mod_subst -open Topconstr type direction = Forward | Backward diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 94bbfce00..b3cfb37fa 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -8,15 +8,11 @@ open Loc open Names -open Decl_kinds open Term open Context open Evd open Environ -open Nametab -open Mod_subst open Constrexpr -open Pp open Globnames type contexts = Parameters | Properties diff --git a/pretyping/typing.ml b/pretyping/typing.ml index bbcc5727b..0cd9099e3 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -14,7 +14,6 @@ open Vars open Environ open Reductionops open Type_errors -open Pretype_errors open Inductive open Inductiveops open Typeops diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index ca370b559..9731e3590 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -6,10 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Environ -open Reduction (** {6 Reduction functions } *) val cbv_vm : env -> constr -> types -> constr |