diff options
| author | Pierre-Marie Pédrot | 2016-05-08 18:59:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-08 19:59:03 +0200 |
| commit | f461e7657cab9917c5b405427ddba3d56f197efb (patch) | |
| tree | 467ac699f78d0360b05174238aeb1177da892503 /parsing | |
| parent | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff) | |
Removing dead code and unused opens.
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 *) |