diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 291bc09650..e7d8249e43 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -25,7 +25,6 @@ open Tactics open Elim open Equality open Misctypes -open Tacexpr open Sigma.Notations open Proofview.Notations @@ -497,8 +496,6 @@ let inversion inv_kind status names id = let inv_gen thin status names = try_intros_until (inversion thin status names) -open Tacexpr - let inv k = inv_gen k NoDep let inv_tac id = inv FullInversion None (NamedHyp id) |