diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 1f3eb13355..e03cc675e7 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -728,7 +728,7 @@ let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in Tacticals.New.tclTHENLIST - [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); + [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 5aff262aa5..7ec1b2ca0c 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1755,7 +1755,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Tacticals.New.tclWITHHOLES false (name_atomic ~env (TacGeneralize cl) - (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma + (Tactics.generalize_gen cl)) sigma end } | TacLetTac (na,c,clp,b,eqpat) -> Proofview.V82.nf_evar_goals <*> |