diff options
Diffstat (limited to 'parsing/egramcoq.mli')
| -rw-r--r-- | parsing/egramcoq.mli | 4 |
1 files changed, 0 insertions, 4 deletions
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 |