diff options
Diffstat (limited to 'parsing/egramcoq.ml')
| -rw-r--r-- | parsing/egramcoq.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index f0c12ab8e..04b622864 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 (**************************************************************************) (* |