Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Remove many superfluous 'open' indicated by ocamlc -w +33

 With ocaml 4.01, the 'unused open' warning also checks the mli :-)

 Beware: some open are reported as useless when compiling with camlp5,
 but are necessary for compatibility with camlp4. These open are now
 marked with a comment.
  • Loading branch information...
commit adfd437f8ae6aaf893119fa4730edecf067dede7 1 parent 3080dd5
@letouzey letouzey authored
Showing with 14 additions and 504 deletions.
  1. +0 −1  checker/closure.mli
  2. +0 −1  checker/environ.mli
  3. +0 −2  checker/indtypes.mli
  4. +0 −1  checker/mod_checking.ml
  5. +0 −1  checker/modops.ml
  6. +0 −1  checker/modops.mli
  7. +0 −1  checker/safe_typing.ml
  8. +0 −1  checker/safe_typing.mli
  9. +0 −1  checker/type_errors.ml
  10. +0 −1  checker/typeops.ml
  11. +0 −2  checker/typeops.mli
  12. +1 −1  grammar/argextend.ml4
  13. +1 −1  grammar/q_constr.ml4
  14. +1 −1  grammar/q_util.mli
  15. +1 −1  grammar/tacextend.ml4
  16. +1 −1  grammar/vernacextend.ml4
  17. +0 −2  ide/gtk_parsing.ml
  18. +0 −1  ide/preferences.ml
  19. +0 −1  ide/utils/editable_cells.ml
  20. +0 −4 ide/wg_ScriptView.ml
  21. +0 −9 interp/constrarg.ml
  22. +0 −1  interp/constrarg.mli
  23. +0 −3  interp/constrexpr_ops.mli
  24. +0 −1  interp/constrextern.ml
  25. +0 −2  interp/constrextern.mli
  26. +0 −1  interp/constrintern.ml
  27. +0 −1  interp/constrintern.mli
  28. +0 −2  interp/coqlib.mli
  29. +0 −2  interp/genintern.ml
  30. +0 −1  interp/implicit_quantifiers.ml
  31. +0 −9 interp/implicit_quantifiers.mli
  32. +0 −1  interp/modintern.ml
  33. +0 −5 interp/modintern.mli
  34. +0 −1  interp/notation.mli
  35. +0 −1  interp/notation_ops.mli
  36. +0 −1  interp/ppextend.mli
  37. +0 −2  interp/reserve.ml
  38. +0 −2  interp/reserve.mli
  39. +0 −1  interp/smartlocate.mli
  40. +0 −1  interp/stdarg.ml
  41. +0 −3  interp/syntax_def.mli
  42. +0 −4 interp/topconstr.mli
  43. +0 −1  intf/tacexpr.mli
  44. +0 −2  intf/vernacexpr.mli
  45. +0 −1  kernel/closure.mli
  46. +0 −4 kernel/constr.ml
  47. +0 −1  kernel/cooking.ml
  48. +0 −2  kernel/cooking.mli
  49. +0 −2  kernel/indtypes.mli
  50. +0 −1  kernel/modops.ml
  51. +0 −1  kernel/modops.mli
  52. +0 −3  kernel/names.ml
  53. +0 −4 kernel/nativeconv.ml
  54. +0 −2  kernel/nativeconv.mli
  55. +0 −3  kernel/nativelambda.mli
  56. +0 −4 kernel/nativelib.ml
  57. +0 −4 kernel/nativelib.mli
  58. +0 −1  kernel/reduction.mli
  59. +0 −1  kernel/retroknowledge.mli
  60. +0 −1  kernel/vconv.mli
  61. +0 −1  kernel/vm.mli
  62. +0 −2  lib/future.ml
  63. +0 −2  lib/pp.mli
  64. +0 −1  library/assumptions.mli
  65. +0 −7 library/declare.mli
  66. +0 −1  library/decls.mli
  67. +0 −3  library/dischargedhypsmap.mli
  68. +0 −1  library/globnames.mli
  69. +0 −3  library/goptions.mli
  70. +0 −1  library/impargs.mli
  71. +3 −6 library/libobject.ml
  72. +0 −1  library/libobject.mli
  73. +0 −2  library/library.mli
  74. +0 −1  parsing/egramcoq.ml
  75. +0 −4 parsing/egramcoq.mli
  76. +0 −1  parsing/egramml.ml
  77. +1 −1  parsing/g_ltac.ml4
  78. +1 −1  parsing/g_prim.ml4
  79. +0 −1  parsing/g_proofs.ml4
  80. +1 −3 parsing/g_vernac.ml4
  81. +1 −3 parsing/g_xml.ml4
  82. +0 −2  parsing/lexer.mli
  83. +1 −2  parsing/pcoq.ml4
  84. +0 −4 parsing/pcoq.mli
  85. +0 −1  plugins/btauto/refl_btauto.ml
  86. +0 −2  plugins/cc/cctac.ml
  87. +0 −1  plugins/decl_mode/decl_expr.mli
  88. +0 −1  plugins/decl_mode/decl_interp.ml
  89. +0 −1  plugins/decl_mode/decl_interp.mli
  90. +0 −1  plugins/decl_mode/decl_mode.mli
  91. +0 −1  plugins/decl_mode/decl_proof_instr.ml
  92. +0 −1  plugins/decl_mode/decl_proof_instr.mli
  93. +1 −1  plugins/decl_mode/g_decl_mode.ml4
  94. +0 −1  plugins/extraction/common.mli
  95. +0 −1  plugins/extraction/extraction.mli
  96. +0 −1  plugins/extraction/mlutil.ml
  97. +0 −1  plugins/extraction/mlutil.mli
  98. +0 −3  plugins/extraction/modutil.mli
  99. +0 −1  plugins/firstorder/ground.ml
  100. +0 −3  plugins/firstorder/instances.mli
  101. +0 −1  plugins/firstorder/sequent.mli
  102. +0 −1  plugins/fourier/fourierR.ml
  103. +0 −1  plugins/funind/functional_principles_types.ml
  104. +0 −1  plugins/funind/g_indfun.ml4
  105. +0 −7 plugins/funind/indfun.mli
  106. +0 −2  plugins/funind/recdef.ml
  107. +0 −1  plugins/omega/coq_omega.ml
  108. +0 −1  plugins/omega/g_omega.ml4
  109. +0 −1  plugins/quote/quote.ml
  110. +0 −1  plugins/romega/g_romega.ml4
  111. +0 −3  plugins/setoid_ring/newring.ml4
  112. +0 −1  pretyping/cases.mli
  113. +0 −1  pretyping/classops.ml
  114. +0 −2  pretyping/classops.mli
  115. +0 −3  pretyping/coercion.mli
  116. +0 −1  pretyping/constrMatching.mli
  117. +0 −2  pretyping/detyping.mli
  118. +0 −2  pretyping/evarconv.mli
  119. +0 −1  pretyping/evarsolve.ml
  120. +0 −1  pretyping/evarutil.ml
  121. +0 −4 pretyping/evarutil.mli
  122. +0 −3  pretyping/evd.mli
  123. +0 −8 pretyping/glob_ops.mli
  124. +0 −2  pretyping/indrec.mli
  125. +0 −1  pretyping/locusops.mli
  126. +0 −3  pretyping/nativenorm.ml
  127. +0 −2  pretyping/nativenorm.mli
  128. +0 −4 pretyping/patternops.mli
  129. +0 −3  pretyping/pretype_errors.ml
  130. +0 −4 pretyping/pretype_errors.mli
  131. +0 −1  pretyping/pretyping.mli
  132. +0 −2  pretyping/recordops.mli
  133. +0 −1  pretyping/reductionops.mli
  134. +0 −1  pretyping/retyping.mli
  135. +0 −1  pretyping/tacred.ml
  136. +0 −3  pretyping/tacred.mli
  137. +0 −2  pretyping/term_dnet.mli
  138. +0 −1  pretyping/termops.mli
  139. +0 −4 pretyping/typeclasses.mli
  140. +0 −4 pretyping/typeclasses_errors.mli
  141. +0 −1  pretyping/typing.ml
  142. +0 −2  pretyping/vnorm.mli
  143. +0 −1  printing/genprint.ml
  144. +0 −2  printing/ppconstr.mli
  145. +0 −1  printing/pptactic.mli
  146. +0 −2  printing/prettyp.mli
  147. +0 −1  printing/printer.ml
  148. +0 −5 printing/printer.mli
  149. +0 −1  printing/printmod.ml
  150. +0 −4 proofs/clenv.mli
  151. +0 −1  proofs/clenvtac.ml
  152. +0 −3  proofs/clenvtac.mli
  153. +0 −5 proofs/evar_refiner.mli
  154. +0 −2  proofs/logic.mli
  155. +0 −1  proofs/pfedit.ml
  156. +0 −4 proofs/pfedit.mli
  157. +0 −2  proofs/proof.mli
  158. +0 −1  proofs/proof_global.ml
  159. +0 −1  proofs/proof_type.ml
  160. +0 −5 proofs/proof_type.mli
  161. +0 −2  proofs/redexpr.mli
  162. +0 −3  proofs/refiner.mli
  163. +0 −2  proofs/tacmach.ml
  164. +0 −6 proofs/tacmach.mli
  165. +0 −2  proofs/tactic_debug.mli
  166. +0 −2  tactics/auto.ml
  167. +0 −2  tactics/auto.mli
  168. +0 −2  tactics/autorewrite.ml
  169. +0 −1  tactics/autorewrite.mli
  170. +0 −1  tactics/contradiction.ml
  171. +0 −2  tactics/contradiction.mli
  172. +0 −4 tactics/eauto.mli
  173. +0 −1  tactics/elim.ml
  174. +0 −3  tactics/elim.mli
  175. +0 −9 tactics/equality.mli
  176. +0 −2  tactics/evar_tactics.ml
  177. +0 −3  tactics/extraargs.mli
  178. +0 −2  tactics/extratactics.mli
  179. +0 −2  tactics/g_class.ml4
  180. +0 −5 tactics/g_rewrite.ml4
  181. +0 −2  tactics/geninterp.ml
  182. +0 −2  tactics/hipattern.mli
  183. +0 −3  tactics/inv.mli
  184. +0 −1  tactics/leminv.ml
  185. +0 −3  tactics/leminv.mli
  186. +0 −10 tactics/rewrite.ml
  187. +0 −2  tactics/taccoerce.ml
  188. +0 −3  tactics/tacintern.ml
  189. +0 −6 tactics/tacintern.mli
  190. +0 −2  tactics/tacinterp.ml
  191. +0 −5 tactics/tacinterp.mli
  192. +0 −1  tactics/tactic_option.mli
  193. +0 −5 tactics/tacticals.mli
  194. +0 −2  tactics/tactics.ml
  195. +0 −9 tactics/tactics.mli
  196. +0 −1  tactics/tauto.ml4
  197. +0 −2  tools/coqdoc/cpretty.mli
  198. +0 −1  toplevel/auto_ind_decl.ml
  199. +0 −4 toplevel/auto_ind_decl.mli
  200. +0 −2  toplevel/autoinstance.mli
  201. +0 −4 toplevel/class.mli
  202. +0 −3  toplevel/classes.ml
  203. +0 −6 toplevel/classes.mli
  204. +0 −2  toplevel/command.mli
  205. +0 −1  toplevel/coqloop.mli
  206. +0 −1  toplevel/discharge.mli
  207. +0 −4 toplevel/himsg.ml
  208. +0 −1  toplevel/himsg.mli
  209. +0 −4 toplevel/ind_tables.mli
  210. +0 −5 toplevel/indschemes.mli
  211. +0 −2  toplevel/lemmas.ml
  212. +0 −1  toplevel/lemmas.mli
  213. +0 −1  toplevel/metasyntax.mli
  214. +0 −4 toplevel/obligations.ml
  215. +0 −4 toplevel/obligations.mli
  216. +0 −1  toplevel/search.ml
  217. +0 −1  toplevel/search.mli
  218. +0 −1  toplevel/vernac.ml
  219. +0 −1  toplevel/vernacentries.ml
  220. +0 −5 toplevel/vernacentries.mli
  221. +0 −2  toplevel/vernacinterp.mli
  222. +0 −2  toplevel/whelp.mli
View
1  checker/closure.mli
@@ -7,7 +7,6 @@
(************************************************************************)
(*i*)
-open Pp
open Names
open Cic
open Esubst
View
1  checker/environ.mli
@@ -1,6 +1,5 @@
open Names
open Cic
-open Term
(* Environments *)
View
2  checker/indtypes.mli
@@ -8,9 +8,7 @@
(*i*)
open Names
-open Univ
open Cic
-open Typeops
open Environ
(*i*)
View
1  checker/mod_checking.ml
@@ -1,6 +1,5 @@
open Pp
-open Errors
open Util
open Names
open Cic
View
1  checker/modops.ml
@@ -12,7 +12,6 @@ open Util
open Pp
open Names
open Cic
-open Term
open Declarations
(*i*)
View
1  checker/modops.mli
@@ -8,7 +8,6 @@
(*i*)
open Names
-open Univ
open Cic
open Environ
(*i*)
View
1  checker/safe_typing.ml
@@ -11,7 +11,6 @@ open Errors
open Util
open Cic
open Names
-open Declarations
open Environ
(************************************************************************)
View
1  checker/safe_typing.mli
@@ -7,7 +7,6 @@
(************************************************************************)
(*i*)
-open Names
open Cic
open Environ
(*i*)
View
1  checker/type_errors.ml
@@ -8,7 +8,6 @@
open Names
open Cic
-open Term
open Environ
type unsafe_judgment = constr * constr
View
1  checker/typeops.ml
@@ -14,7 +14,6 @@ open Cic
open Term
open Reduction
open Type_errors
-open Declarations
open Inductive
open Environ
View
2  checker/typeops.mli
@@ -7,9 +7,7 @@
(************************************************************************)
(*i*)
-open Names
open Cic
-open Term
open Environ
(*i*)
View
2  grammar/argextend.ml4
@@ -232,7 +232,7 @@ let declare_vernac_argument loc s pr cl =
open Pcoq
open Pcaml
-open PcamlSig
+open PcamlSig (* necessary for camlp4 *)
EXTEND
GLOBAL: str_item;
View
2  grammar/q_constr.ml4
@@ -11,7 +11,7 @@
open Q_util
open Compat
open Pcaml
-open PcamlSig
+open PcamlSig (* necessary for camlp4 *)
let loc = CompatLoc.ghost
let dloc = <:expr< Loc.ghost >>
View
2  grammar/q_util.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Compat
+open Compat (* necessary for camlp4 *)
val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr
View
2  grammar/tacextend.ml4
@@ -186,7 +186,7 @@ let declare_tactic loc s c cl =
]
open Pcaml
-open PcamlSig
+open PcamlSig (* necessary for camlp4 *)
EXTEND
GLOBAL: str_item;
View
2  grammar/vernacextend.ml4
@@ -113,7 +113,7 @@ let declare_command loc s c nt cl =
} >> ]
open Pcaml
-open PcamlSig
+open PcamlSig (* necessary for camlp4 *)
EXTEND
GLOBAL: str_item;
View
2  ide/gtk_parsing.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Ideutils
-
let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0)
let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0)
View
1  ide/preferences.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Configwin
-open Printf
let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc"
let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys"
View
1  ide/utils/editable_cells.ml
@@ -1,4 +1,3 @@
-open GTree
open Gobject
let create l =
View
4 ide/wg_ScriptView.ml
@@ -6,10 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Ideutils
-open GText
-open Gtk_parsing
-
type insert_action = {
ins_val : string;
ins_off : int;
View
9 interp/constrarg.ml
@@ -7,16 +7,7 @@
(************************************************************************)
open Loc
-open Pp
-open Names
-open Term
-open Libnames
-open Globnames
-open Glob_term
-open Genredexpr
open Tacexpr
-open Pattern
-open Constrexpr
open Term
open Misctypes
open Genarg
View
1  interp/constrarg.mli
@@ -14,7 +14,6 @@ open Names
open Term
open Libnames
open Globnames
-open Glob_term
open Genredexpr
open Pattern
open Constrexpr
View
3  interp/constrexpr_ops.mli
@@ -7,12 +7,9 @@
(************************************************************************)
open Loc
-open Pp
open Names
open Libnames
open Misctypes
-open Term
-open Mod_subst
open Constrexpr
(** Constrexpr_ops: utilities on [constr_expr] *)
View
1  interp/constrextern.ml
@@ -26,7 +26,6 @@ open Glob_ops
open Pattern
open Nametab
open Notation
-open Reserve
open Detyping
open Misctypes
open Decl_kinds
View
2  interp/constrextern.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Names
open Term
open Context
@@ -14,7 +13,6 @@ open Termops
open Environ
open Libnames
open Globnames
-open Nametab
open Glob_term
open Pattern
open Constrexpr
View
1  interp/constrintern.ml
@@ -9,7 +9,6 @@
open Pp
open Errors
open Util
-open Flags
open Names
open Nameops
open Namegen
View
1  interp/constrintern.mli
@@ -17,7 +17,6 @@ open Glob_term
open Pattern
open Constrexpr
open Notation_term
-open Termops
open Pretyping
open Misctypes
open Decl_kinds
View
2  interp/coqlib.mli
@@ -9,9 +9,7 @@
open Names
open Libnames
open Globnames
-open Nametab
open Term
-open Pattern
open Util
(** This module collects the global references, constructions and
View
2  interp/genintern.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
-open Util
open Names
open Mod_subst
open Genarg
View
1  interp/implicit_quantifiers.ml
@@ -14,7 +14,6 @@ open Util
open Glob_term
open Constrexpr
open Libnames
-open Globnames
open Typeclasses
open Typeclasses_errors
open Pp
View
9 interp/implicit_quantifiers.mli
@@ -8,19 +8,10 @@
open Loc
open Names
-open Decl_kinds
-open Term
-open Context
-open Evd
-open Environ
-open Nametab
-open Mod_subst
open Glob_term
open Constrexpr
-open Pp
open Libnames
open Globnames
-open Typeclasses
val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
View
1  interp/modintern.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Declarations
-open Entries
open Libnames
open Constrexpr
open Constrintern
View
5 interp/modintern.mli
@@ -6,13 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Loc
-open Declarations
open Environ
open Entries
-open Pp
-open Libnames
-open Names
open Constrexpr
open Misctypes
View
1  interp/notation.mli
@@ -9,7 +9,6 @@
open Pp
open Bigint
open Names
-open Nametab
open Libnames
open Globnames
open Constrexpr
View
1  interp/notation_ops.mli
@@ -8,7 +8,6 @@
open Names
open Notation_term
-open Misctypes
open Glob_term
(** Utilities about [notation_constr] *)
View
1  interp/ppextend.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Pp
-open Names
(** {6 Pretty-print. } *)
View
2  interp/reserve.ml
@@ -123,8 +123,6 @@ let revert_reserved_type t =
let _ = Namegen.set_reserved_typed_name revert_reserved_type
-open Glob_term
-
let default_env () = {
ninterp_var_type = Id.Map.empty;
ninterp_rec_vars = Id.Map.empty;
View
2  interp/reserve.mli
@@ -7,9 +7,7 @@
(************************************************************************)
open Loc
-open Pp
open Names
-open Glob_term
open Notation_term
val declare_reserved_type : Id.t located list -> notation_constr -> unit
View
1  interp/smartlocate.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Loc
-open Pp
open Names
open Libnames
open Globnames
View
1  interp/stdarg.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Genarg
let wit_unit : unit uniform_genarg_type =
View
3  interp/syntax_def.mli
@@ -8,9 +8,6 @@
open Names
open Notation_term
-open Glob_term
-open Nametab
-open Libnames
(** Syntactic definitions. *)
View
4 interp/topconstr.mli
@@ -8,11 +8,7 @@
open Loc
open Names
-open Libnames
-open Misctypes
-open Decl_kinds
open Constrexpr
-open Notation_term
(** Topconstr *)
View
1  intf/tacexpr.mli
@@ -18,7 +18,6 @@ open Pattern
open Decl_kinds
open Misctypes
open Locus
-open Pp
type 'a or_metaid = AI of 'a | MetaId of Loc.t * string
View
2  intf/vernacexpr.mli
@@ -7,8 +7,6 @@
(************************************************************************)
open Loc
-open Pp
-open Util
open Names
open Tacexpr
open Misctypes
View
1  kernel/closure.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Names
open Term
open Environ
View
4 kernel/constr.ml
@@ -23,12 +23,8 @@
Inductive Constructions (CIC) terms together with constructors,
destructors, iterators and basic functions *)
-open Errors
open Util
-open Pp
open Names
-open Univ
-open Esubst
type existential_key = Evar.t
View
1  kernel/cooking.ml
@@ -17,7 +17,6 @@ open Errors
open Util
open Names
open Term
-open Context
open Declarations
open Environ
View
2  kernel/cooking.mli
@@ -6,11 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open Term
open Declarations
open Environ
-open Univ
(** {6 Cooking the constants. } *)
View
2  kernel/indtypes.mli
@@ -7,12 +7,10 @@
(************************************************************************)
open Names
-open Univ
open Term
open Declarations
open Environ
open Entries
-open Typeops
(** Inductive type checking and errors *)
View
1  kernel/modops.ml
@@ -15,7 +15,6 @@
(* This file provides with various operations on modules and module types *)
-open Errors
open Util
open Names
open Term
View
1  kernel/modops.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Univ
open Term
open Environ
open Declarations
View
3  kernel/names.ml
@@ -19,7 +19,6 @@
Élie Soubiran, ... *)
open Pp
-open Errors
open Util
(** {6 Identifiers } *)
@@ -485,8 +484,6 @@ module KerPair = struct
the same user part implies having the same canonical part
(invariant of the system). *)
- open Hashset.Combine
-
let hash = function
| Same kn -> KerName.hash kn
| Dual (kn, _) -> KerName.hash kn
View
4 kernel/nativeconv.ml
@@ -7,15 +7,11 @@
(************************************************************************)
open Errors
open Names
-open Term
open Univ
-open Pre_env
open Nativelib
open Reduction
-open Declarations
open Util
open Nativevalues
-open Nativelambda
open Nativecode
(** This module implements the conversion test by compiling to OCaml code *)
View
2  kernel/nativeconv.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Term
-open Univ
-open Environ
open Reduction
open Nativelambda
View
3  kernel/nativelambda.mli
@@ -5,11 +5,8 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Util
open Names
-open Esubst
open Term
-open Declarations
open Pre_env
open Nativevalues
View
4 kernel/nativelib.ml
@@ -5,13 +5,9 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
-open Term
open Util
open Nativevalues
-open Declarations
open Nativecode
-open Pre_env
open Errors
open Envars
View
4 kernel/nativelib.mli
@@ -5,11 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
-open Term
-open Nativevalues
open Nativecode
-open Pre_env
(** This file provides facilities to access OCaml compiler and dynamic linker,
used by the native compiler. *)
View
1  kernel/reduction.mli
@@ -9,7 +9,6 @@
open Term
open Context
open Environ
-open Closure
(***********************************************************************
s Reduction functions *)
View
1  kernel/retroknowledge.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open Term
type retroknowledge
View
1  kernel/vconv.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open Term
open Environ
open Reduction
View
1  kernel/vm.mli
@@ -1,7 +1,6 @@
open Names
open Term
open Cbytecodes
-open Cemitcodes
(** Efficient Virtual Machine *)
View
2  lib/future.ml
@@ -40,8 +40,6 @@ module UUID = struct
let equal = (==)
end
-open UUID
-
type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
(* Val is not necessarily a final state, so the
View
2  lib/pp.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp_control
-
(** Modify pretty printing functions behavior for emacs ouput (special
chars inserted at some places). This function should called once in
module [Options], that's all. *)
View
1  library/assumptions.mli
@@ -9,7 +9,6 @@
open Util
open Names
open Term
-open Environ
(** A few declarations for the "Print Assumption" command
@author spiwack *)
View
7 library/declare.mli
@@ -9,12 +9,7 @@
open Names
open Libnames
open Term
-open Context
-open Declarations
open Entries
-open Indtypes
-open Safe_typing
-open Nametab
open Decl_kinds
(** This module provides the official functions to declare new variables,
@@ -24,8 +19,6 @@ open Decl_kinds
reset works properly --- and will fill some global tables such as
[Nametab] and [Impargs]. *)
-open Nametab
-
(** Declaration of local constructions (Variable/Hypothesis/Local) *)
type section_variable_entry =
View
1  library/decls.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Context
open Libnames
open Decl_kinds
View
3  library/dischargedhypsmap.mli
@@ -7,9 +7,6 @@
(************************************************************************)
open Libnames
-open Term
-open Environ
-open Nametab
type discharged_hyps = full_path list
View
1  library/globnames.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Util
-open Pp
open Names
open Term
open Mod_subst
View
3  library/goptions.mli
@@ -44,10 +44,7 @@
(synchronous = consistent with the resetting commands) *)
open Pp
-open Names
open Libnames
-open Term
-open Nametab
open Mod_subst
type option_name = Interface.option_name
View
1  library/impargs.mli
@@ -10,7 +10,6 @@ open Names
open Globnames
open Term
open Environ
-open Nametab
(** {6 Implicit Arguments } *)
(** Here we store the implicit arguments. Notice that we
View
9 library/libobject.ml
@@ -6,10 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Util
-open Errors
open Libnames
-open Mod_subst
(* The relax flag is used to make it possible to load files while ignoring
failures to incorporate some objects. This can be useful when one
@@ -32,11 +29,11 @@ type 'a object_declaration = {
load_function : int -> object_name * 'a -> unit;
open_function : int -> object_name * 'a -> unit;
classify_function : 'a -> 'a substitutivity;
- subst_function : substitution * 'a -> 'a;
+ subst_function : Mod_subst.substitution * 'a -> 'a;
discharge_function : object_name * 'a -> 'a option;
rebuild_function : 'a -> 'a }
-let yell s = anomaly (Pp.str s)
+let yell s = Errors.anomaly (Pp.str s)
let default_object s = {
object_name = s;
@@ -69,7 +66,7 @@ type dynamic_object_declaration = {
dyn_cache_function : object_name * obj -> unit;
dyn_load_function : int -> object_name * obj -> unit;
dyn_open_function : int -> object_name * obj -> unit;
- dyn_subst_function : substitution * obj -> obj;
+ dyn_subst_function : Mod_subst.substitution * obj -> obj;
dyn_classify_function : obj -> obj substitutivity;
dyn_discharge_function : object_name * obj -> obj option;
dyn_rebuild_function : obj -> obj }
View
1  library/libobject.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
open Libnames
open Mod_subst
View
2  library/library.mli
@@ -7,10 +7,8 @@
(************************************************************************)
open Loc
-open Pp
open Names
open Libnames
-open Libobject
(** This module provides functions to load, open and save
libraries. Libraries correspond to the subclass of modules that
View
1  parsing/egramcoq.ml
@@ -11,7 +11,6 @@ open Errors
open Util
open Pcoq
open Extend
-open Ppextend
open Constrexpr
open Notation_term
open Libnames
View
4 parsing/egramcoq.mli
@@ -6,15 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Compat
-open Pp
open Names
open Constrexpr
open Notation_term
open Pcoq
open Extend
-open Vernacexpr
-open Ppextend
open Genarg
open Egramml
View
1  parsing/egramml.ml
@@ -10,7 +10,6 @@ open Compat
open Names
open Pcoq
open Genarg
-open Tacexpr
open Vernacexpr
(** Making generic actions in type generic_argument *)
View
2  parsing/g_ltac.ml4
@@ -13,7 +13,7 @@ open Tacexpr
open Misctypes
open Genarg
open Genredexpr
-open Tok
+open Tok (* necessary for camlp4 *)
open Pcoq
open Pcoq.Prim
View
2  parsing/g_prim.ml4
@@ -9,7 +9,7 @@
open Compat
open Names
open Libnames
-open Tok
+open Tok (* necessary for camlp4 *)
open Pcoq
open Pcoq.Prim
View
1  parsing/g_proofs.ml4
@@ -9,7 +9,6 @@
open Compat
open Constrexpr
open Vernacexpr
-open Locality
open Misctypes
open Tok
View
4 parsing/g_vernac.ml4
@@ -8,7 +8,6 @@
open Pp
open Compat
-open Tok
open Errors
open Util
open Names
@@ -16,10 +15,9 @@ open Constrexpr
open Constrexpr_ops
open Extend
open Vernacexpr
-open Locality
open Decl_kinds
-open Declaremods
open Misctypes
+open Tok (* necessary for camlp4 *)
open Pcoq
open Pcoq.Tactic
View
4 parsing/g_xml.ml4
@@ -16,13 +16,11 @@ open Glob_term
open Tacexpr
open Libnames
open Globnames
-
-open Nametab
open Detyping
-open Tok
open Misctypes
open Decl_kinds
open Genredexpr
+open Tok (* necessary for camlp4 *)
(* Generic xml parser without raw data *)
View
2  parsing/lexer.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
-
val add_keyword : string -> unit
val remove_keyword : string -> unit
val is_keyword : string -> bool
View
3  parsing/pcoq.ml4
@@ -8,14 +8,13 @@
open Pp
open Compat
-open Tok
open Errors
open Util
open Extend
open Genarg
open Stdarg
open Constrarg
-open Tacexpr
+open Tok (* necessary for camlp4 *)
(** The parser of Coq *)
View
4 parsing/pcoq.mli
@@ -7,9 +7,7 @@
(************************************************************************)
open Loc
-open Pp
open Names
-open Glob_term
open Extend
open Vernacexpr
open Genarg
@@ -211,7 +209,6 @@ module Module :
module Tactic :
sig
- open Glob_term
val open_constr : open_constr_expr Gram.entry
val constr_with_bindings : constr_expr with_bindings Gram.entry
val bindings : constr_expr bindings Gram.entry
@@ -231,7 +228,6 @@ module Tactic :
module Vernac_ :
sig
- open Decl_kinds
val gallina : vernac_expr Gram.entry
val gallina_ext : vernac_expr Gram.entry
val command : vernac_expr Gram.entry
View
1  plugins/btauto/refl_btauto.ml
@@ -1,4 +1,3 @@
-open Proofview.Notations
let contrib_name = "btauto"
View
2  plugins/cc/cctac.ml
@@ -16,14 +16,12 @@ open Term
open Vars
open Tacmach
open Tactics
-open Tacticals
open Typing
open Ccalgo
open Ccproof
open Pp
open Errors
open Util
-open Proofview.Notations
let constant dir s = lazy (Coqlib.gen_constant "CC" dir s)
View
1  plugins/decl_mode/decl_expr.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Pp
open Tacexpr
type 'it statement =
View
1  plugins/decl_mode/decl_interp.ml
@@ -11,7 +11,6 @@ open Util
open Names
open Constrexpr
open Tacintern
-open Tacinterp
open Decl_expr
open Decl_mode
open Pretyping
View
1  plugins/decl_mode/decl_interp.mli
@@ -8,7 +8,6 @@
open Tacintern
open Decl_expr
-open Mod_subst
val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr
View
1  plugins/decl_mode/decl_mode.mli
@@ -9,7 +9,6 @@
open Names
open Term
open Evd
-open Tacmach
val set_daimon_flag : unit -> unit
val clear_daimon_flag : unit -> unit
View
1  plugins/decl_mode/decl_proof_instr.ml
@@ -13,7 +13,6 @@ open Evd
open Tacmach
open Tacintern
-open Tacinterp
open Decl_expr
open Decl_mode
open Decl_interp
View
1  plugins/decl_mode/decl_proof_instr.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Refiner
open Names
open Term
open Tacmach
View
2  plugins/decl_mode/g_decl_mode.ml4
@@ -11,11 +11,11 @@
open Util
open Compat
open Pp
-open Tok
open Decl_expr
open Names
open Pcoq
open Vernacexpr
+open Tok (* necessary for camlp4 *)
open Pcoq.Constr
open Pcoq.Tactic
View
1  plugins/extraction/common.mli
@@ -9,7 +9,6 @@
open Names
open Globnames
open Miniml
-open Mlutil
open Pp
(** By default, in module Format, you can do horizontal placing of blocks
View
1  plugins/extraction/extraction.mli
@@ -12,7 +12,6 @@ open Names
open Term
open Declarations
open Environ
-open Libnames
open Miniml
val extract_constant : env -> constant -> constant_body -> ml_decl
View
1  plugins/extraction/mlutil.ml
@@ -1363,7 +1363,6 @@ let is_not_strict t =
restriction for the moment.
*)
-open Declarations
open Declareops
let inline_test r t =
View
1  plugins/extraction/mlutil.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Term
open Globnames
open Miniml
open Table
View
3  plugins/extraction/modutil.mli
@@ -7,11 +7,8 @@
(************************************************************************)
open Names
-open Declarations
-open Environ
open Globnames
open Miniml
-open Mod_subst
(*s Functions upon ML modules. *)
View
1  plugins/firstorder/ground.ml
@@ -11,7 +11,6 @@ open Sequent
open Rules
open Instances
open Term
-open Vars
open Tacmach
open Tacticals
View
3  plugins/firstorder/instances.mli
@@ -6,9 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
-open Tacmach
-open Names
open Globnames
open Rules
View
1  plugins/firstorder/sequent.mli
@@ -9,7 +9,6 @@
open Term
open Formula
open Tacmach
-open Names
open Globnames
module OrderedConstr: Set.OrderedType with type t=constr
View
1  plugins/fourier/fourierR.ml
@@ -15,7 +15,6 @@ des in
open Term
open Tactics
open Names
-open Libnames
open Globnames
open Tacticals
open Tacmach
View
1  plugins/funind/functional_principles_types.ml
@@ -6,7 +6,6 @@ open Vars
open Context
open Namegen
open Names
-open Declarations
open Declareops
open Pp
open Entries
View
1  plugins/funind/g_indfun.ml4
@@ -18,7 +18,6 @@ open Indfun
open Genarg
open Tacticals
open Misctypes
-open Miscops
let pr_binding prc = function
| loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
View
7 plugins/funind/indfun.mli
@@ -1,10 +1,3 @@
-open Names
-open Term
-open Pp
-open Indfun_common
-open Libnames
-open Glob_term
-open Declarations
open Misctypes
val do_generate_principle :
View
2  plugins/funind/recdef.ml
@@ -10,7 +10,6 @@ open Term
open Vars
open Namegen
open Environ
-open Declarations
open Declareops
open Entries
open Pp
@@ -24,7 +23,6 @@ open Tacticals
open Tacmach
open Tactics
open Nametab
-open Decls
open Declare
open Decl_kinds
open Tacred
View
1  plugins/omega/coq_omega.ml
@@ -27,7 +27,6 @@ open Globnames
open Nametab
open Contradiction
open Misctypes
-open Proofview.Notations
module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
open OmegaSolver
View
1  plugins/omega/g_omega.ml4
@@ -16,7 +16,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Coq_omega
-open Refiner
let omega_tactic l =
let tacs = List.map
View
1  plugins/quote/quote.ml
@@ -109,7 +109,6 @@ open Pattern
open Patternops
open ConstrMatching
open Tacmach
-open Proofview.Notations
(*i*)
(*s First, we need to access some Coq constants
View
1  plugins/romega/g_romega.ml4
@@ -9,7 +9,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Refl_omega
-open Refiner
let romega_tactic l =
let tacs = List.map
View
3  plugins/setoid_ring/newring.ml4
@@ -22,7 +22,6 @@ open Glob_term
open Tacticals
open Tacexpr
open Coqlib
-open Tacmach
open Mod_subst
open Tacinterp
open Libobject
@@ -797,8 +796,6 @@ let ltac_ring_structure e =
[req;sth;ext;morph;th;cst_tac;pow_tac;
lemma1;lemma2;pretac;posttac]
-open Proofview.Notations
-
let ring_lookup (f:glob_tactic_expr) lH rl t =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
View
1  pretyping/cases.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Names
open Term
open Context
View
1  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 *)
View
2  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 } *)
View
3  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. } *)
View
1  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 *)
View
2  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
View
2  pretyping/evarconv.mli
@@ -8,9 +8,7 @@
open Names
open Term
-open Context
open Environ
-open Termops
open Reductionops
open Evd
open Locus
View
1  pretyping/evarsolve.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Util
open Errors
open Names
View
1  pretyping/evarutil.ml
@@ -20,7 +20,6 @@ open Environ
open Evd
open Reductionops
open Pretype_errors
-open Retyping
(****************************************************)
(* Expanding/testing/exposing existential variables *)
View
4 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 } *)
View
3  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}
View
8 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 *)
View
2  pretyping/indrec.mli
@@ -8,8 +8,6 @@
open Names
open Term
-open Declarations
-open Inductiveops
open Environ
open Evd
View
1  pretyping/locusops.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Misctypes
open Locus
(** Utilities on occurrences *)
View
3  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
View
2  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
View
4 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
View
3  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
View
4 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 } *)
View
1  pretyping/pretyping.mli
@@ -13,7 +13,6 @@
implicit arguments. *)
open Names
-open Context
open Term
open Environ
open Evd
View
2  pretyping/recordops.mli
@@ -7,10 +7,8 @@
(************************************************************************)
open Names
-open Nametab
open Term