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 9aa417a09..3245c642f 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 19e8ee8f6..ee6ed4a9e 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 dc558e841..f26ff817b 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 c2dbd1d63..58def67b6 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 f30ebfb7c..d41fcb7ae 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 dc545c691..e95aecca8 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 371dae6c8..b52dcdbd6 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 a32a40f9d..820d44392 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 8eef2f63c..dd811acfe 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 6dee6cf16..6fac3da96 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 5dcfa844a..3fb647a96 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 |