diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 0c89eb3a2..49d40db24 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -6,16 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names -open Proof_type -open Tacmach open Tactic_debug open Term open Tacexpr open Genarg -open Constrexpr -open Mod_subst open Redexpr open Misctypes |