diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/egramml.ml | 2 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 1 |
4 files changed, 0 insertions, 6 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index f0c12ab8ef..04b6228643 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -14,9 +14,7 @@ open Extend open Constrexpr open Notation_term open Libnames -open Tacexpr open Names -open Egramml (**************************************************************************) (* diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 37fccdb3c2..95ac872473 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -7,8 +7,6 @@ (************************************************************************) open Util -open Compat -open Names open Extend open Pcoq open Genarg diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 1c39858ea7..35ba9757d4 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -20,7 +20,6 @@ open Misctypes open Tok (* necessary for camlp4 *) open Pcoq -open Pcoq.Tactic open Pcoq.Prim open Pcoq.Constr open Pcoq.Vernac_ diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 53d2089c04..fe9ab630fa 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -12,7 +12,6 @@ open Errors open Util open Extend open Genarg -open Tok (* necessary for camlp4 *) (** The parser of Coq *) |