diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 3 | ||||
| -rw-r--r-- | parsing/egramml.ml | 1 | ||||
| -rw-r--r-- | parsing/extrawit.ml | 1 |
3 files changed, 0 insertions, 5 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 4cfc730a92..488c425cc5 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Compat open Errors open Util @@ -15,11 +14,9 @@ open Extend open Ppextend open Constrexpr open Notation_term -open Genarg open Libnames open Tacexpr open Names -open Vernacexpr open Egramml (**************************************************************************) diff --git a/parsing/egramml.ml b/parsing/egramml.ml index abd1bcd5b5..c74f369075 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Compat open Names open Pcoq diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index 75205c9644..e7d9ba4b2f 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors -open Util open Genarg (* This file defines extra argument types *) |