aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml1
-rw-r--r--toplevel/auto_ind_decl.mli4
-rw-r--r--toplevel/autoinstance.mli2
-rw-r--r--toplevel/class.mli4
-rw-r--r--toplevel/classes.ml3
-rw-r--r--toplevel/classes.mli6
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/coqloop.mli1
-rw-r--r--toplevel/discharge.mli1
-rw-r--r--toplevel/himsg.ml4
-rw-r--r--toplevel/himsg.mli1
-rw-r--r--toplevel/ind_tables.mli4
-rw-r--r--toplevel/indschemes.mli5
-rw-r--r--toplevel/lemmas.ml2
-rw-r--r--toplevel/lemmas.mli1
-rw-r--r--toplevel/metasyntax.mli1
-rw-r--r--toplevel/obligations.ml4
-rw-r--r--toplevel/obligations.mli4
-rw-r--r--toplevel/search.ml1
-rw-r--r--toplevel/search.mli1
-rw-r--r--toplevel/vernac.ml1
-rw-r--r--toplevel/vernacentries.ml1
-rw-r--r--toplevel/vernacentries.mli5
-rw-r--r--toplevel/vernacinterp.mli2
-rw-r--r--toplevel/whelp.mli2
25 files changed, 0 insertions, 63 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b79d77443..94447f0d0 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -21,7 +21,6 @@ open Names
open Globnames
open Inductiveops
open Tactics
-open Tacticals
open Ind_tables
open Misctypes
open Proofview.Notations
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 660f6f7e7..6509a7d3b 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -8,10 +8,6 @@
open Term
open Names
-open Libnames
-open Mod_subst
-open Context
-open Proof_type
open Ind_tables
(** This file is about the automatic generation of schemes about
diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
index ebaaee12d..bfc9bcff2 100644
--- a/toplevel/autoinstance.mli
+++ b/toplevel/autoinstance.mli
@@ -8,8 +8,6 @@
open Term
open Globnames
-open Typeclasses
-open Names
open Evd
open Context
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 0d39ee170..8bb3eb7ce 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -7,12 +7,8 @@
(************************************************************************)
open Names
-open Term
open Classops
-open Declare
open Globnames
-open Decl_kinds
-open Nametab
(** Classes and coercions. *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 220e0e050..4d8a6d5d7 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -10,8 +10,6 @@
open Names
open Term
open Vars
-open Context
-open Evd
open Environ
open Nametab
open Errors
@@ -26,7 +24,6 @@ open Constrexpr
open Decl_kinds
open Entries
-open Misctypes
let typeclasses_db = "typeclass_instances"
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index a8e611928..de62ff369 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -7,18 +7,12 @@
(************************************************************************)
open Names
-open Decl_kinds
-open Term
open Context
open Evd
open Environ
-open Nametab
-open Mod_subst
open Constrexpr
open Typeclasses
-open Implicit_quantifiers
open Libnames
-open Globnames
(** Errors *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index fe6a0a400..d2ebdc561 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Names
open Term
open Entries
@@ -17,7 +16,6 @@ open Vernacexpr
open Constrexpr
open Decl_kinds
open Redexpr
-open Constrintern
open Pfedit
(** This file is about the interpretation of raw commands into typed
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 1375f3361..4aedaa035 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Pp
-open Pcoq
(** The Coq toplevel loop. *)
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 6f696f27a..6cef31c8a 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Context
-open Cooking
open Declarations
open Entries
open Opaqueproof
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 5d024d31c..303b3f8d6 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -14,7 +14,6 @@ open Namegen
open Term
open Termops
open Indtypes
-open Context
open Environ
open Pretype_errors
open Type_errors
@@ -24,9 +23,6 @@ open Cases
open Logic
open Printer
open Evd
-open Libnames
-open Globnames
-open Declarations
(* This simplifies the typing context of Cases clauses *)
(* hope it does not disturb other typing contexts *)
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 9ec344405..bdc3eb707 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Pp
-open Names
open Indtypes
open Environ
open Type_errors
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index c5e82e2e2..d57f1556d 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -8,10 +8,6 @@
open Term
open Names
-open Libnames
-open Mod_subst
-open Context
-open Declarations
(** This module provides support for registering inductive scheme builders,
declaring schemes and generating schemes on demand *)
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index be49f41e5..7abae933d 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -7,15 +7,10 @@
(************************************************************************)
open Loc
-open Pp
open Names
open Term
open Environ
-open Libnames
-open Glob_term
-open Genarg
open Vernacexpr
-open Ind_tables
open Misctypes
(** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index f6cf147ab..fd606a6b8 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -27,12 +27,10 @@ open Declare
open Pretyping
open Termops
open Namegen
-open Evarutil
open Reductionops
open Constrexpr
open Constrintern
open Impargs
-open Tacticals
(* Support for mutually proved theorems *)
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index aea5c95cf..bbe383a85 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -12,7 +12,6 @@ open Decl_kinds
open Constrexpr
open Tacexpr
open Vernacexpr
-open Proof_type
open Pfedit
(** A hook start_proof calls on the type of the definition being started *)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 93752b3bc..20326c9c8 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Libnames
open Tacexpr
open Vernacexpr
open Notation
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 6536796f4..d772af3c1 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -20,7 +20,6 @@ open Evd
open Pp
open Errors
open Util
-open Proof_type
let declare_fix_ref = ref (fun _ _ _ _ _ -> assert false)
let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
@@ -143,9 +142,6 @@ let etype_of_evar evs hyps concl =
subst_vars acc 0 t', s, trans
in aux [] 0 (List.rev hyps)
-
-open Tacticals
-
let trunc_named_context n ctx =
let len = List.length ctx in
List.firstn (len - n) ctx
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 04292422c..746b4ed14 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -7,15 +7,11 @@
(************************************************************************)
open Environ
-open Tacmach
open Term
open Evd
open Names
open Pp
-open Util
-open Tacinterp
open Globnames
-open Proof_type
open Vernacexpr
open Decl_kinds
open Tacexpr
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 78fa3a325..72528675c 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Pp
-open Errors
open Util
open Names
open Term
diff --git a/toplevel/search.mli b/toplevel/search.mli
index c139c71cd..c06a64be1 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -12,7 +12,6 @@ open Term
open Environ
open Pattern
open Globnames
-open Nametab
(** {6 Search facilities. } *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index b35929fef..667a60058 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -14,7 +14,6 @@ open Util
open Flags
open System
open Vernacexpr
-open Vernacinterp
(* The functions in this module may raise (unexplainable!) exceptions.
Use the module Coqtoplevel, which catches these exceptions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index cd38510f3..395119083 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -30,7 +30,6 @@ open Decl_kinds
open Constrexpr
open Redexpr
open Lemmas
-open Declaremods
open Misctypes
open Locality
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 3f6d45a04..9b49e5772 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -6,11 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
-open Term
-open Vernacinterp
-open Vernacexpr
-open Constrexpr
open Misctypes
val dump_global : Libnames.reference or_by_notation -> unit
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 8f8f5bdd7..3cbbbf05e 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Tacexpr
-
(** Interpretation of extended vernac phrases. *)
val vinterp_add : string -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli
index fed8332bd..ab8069ec6 100644
--- a/toplevel/whelp.mli
+++ b/toplevel/whelp.mli
@@ -11,8 +11,6 @@
open Names
open Term
-open Topconstr
-open Environ
type whelp_request =
| Locate of string
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 06:04:15 +0000