diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index e0ed2d1ef..b6923bb83 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -469,7 +469,7 @@ let raw_inversion inv_kind id status names gl = case_nodep_then_using in (tclTHENS - (true_cut Anonymous cut_concl) + (assert_tac Anonymous cut_concl) [case_tac names (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) (Some elim_predicate) ([],[]) ind indclause; |