diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 150e0050c..aaa75a4e2 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -14,20 +14,9 @@ open Term open Termops open Sign open Declarations -open Inductive -open Reduction -open Environ -open Libnames -open Refiner open Tacmach open Clenv open Clenvtac -open Glob_term -open Pattern -open Matching -open Genarg -open Tacexpr -open Locus open Misctypes (************************************************************************) |