diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 1 | ||||
| -rw-r--r-- | parsing/egramcoq.mli | 4 | ||||
| -rw-r--r-- | parsing/egramml.ml | 1 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_prim.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/g_xml.ml4 | 4 | ||||
| -rw-r--r-- | parsing/lexer.mli | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 4 |
11 files changed, 5 insertions, 23 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 9aa417a094..3245c642fa 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -11,7 +11,6 @@ open Errors open Util open Pcoq open Extend -open Ppextend open Constrexpr open Notation_term open Libnames diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 19e8ee8f60..ee6ed4a9ed 100644 --- a/parsing/egramcoq.mli +++ b/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 diff --git a/parsing/egramml.ml b/parsing/egramml.ml index dc558e8416..f26ff817b2 100644 --- a/parsing/egramml.ml +++ b/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 *) diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index c2dbd1d63e..58def67b68 100644 --- a/parsing/g_ltac.ml4 +++ b/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 diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index f30ebfb7c0..d41fcb7aea 100644 --- a/parsing/g_prim.ml4 +++ b/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 diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index dc545c691f..e95aecca83 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -9,7 +9,6 @@ open Compat open Constrexpr open Vernacexpr -open Locality open Misctypes open Tok diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 371dae6c81..b52dcdbd60 100644 --- a/parsing/g_vernac.ml4 +++ b/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 diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index a32a40f9dc..820d44392b 100644 --- a/parsing/g_xml.ml4 +++ b/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 *) diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 8eef2f63c3..dd811acfe9 100644 --- a/parsing/lexer.mli +++ b/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 diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6dee6cf160..6fac3da965 100644 --- a/parsing/pcoq.ml4 +++ b/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 *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 5dcfa844a4..3fb647a96c 100644 --- a/parsing/pcoq.mli +++ b/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 |