diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0e802f8a9..60564dbdb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -7,7 +7,6 @@ (************************************************************************) open Constrintern -open Pattern open Patternops open Pp open Genredexpr @@ -37,7 +36,6 @@ open Printer open Pretyping open Evd open Misctypes -open Miscops open Locus open Tacintern open Taccoerce |