diff options
Diffstat (limited to 'ltac/tacsubst.ml')
| -rw-r--r-- | ltac/tacsubst.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 54d32f266..1326818fc 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -16,7 +16,6 @@ open Globnames open Term open Genredexpr open Patternops -open Pretyping (** Substitution of tactics at module closing time *) |