diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 6c63a891e8..d138ae755a 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -736,7 +736,7 @@ let refl_equal () = Coqlib.lib_ref "core.eq.type" call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in + let type_of_a = Tacmach.New.pf_get_type_of gl a in Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> Tacticals.New.tclTHENLIST [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; |