diff options
Diffstat (limited to 'ltac/tacenv.ml')
| -rw-r--r-- | ltac/tacenv.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index f2dbb5b6c..39db6268b 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -7,11 +7,9 @@ (************************************************************************) open Util -open Genarg open Pp open Names open Tacexpr -open Geninterp (** Tactic notations (TacAlias) *) |