diff options
| author | Gaëtan Gilbert | 2020-02-06 20:29:55 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | aa0f5e5cf23a650bf0302d2c35aa2b0d56f59f48 (patch) | |
| tree | 69d4d427406c5df7b39392580d03d874dd410d11 /plugins | |
| parent | b0b473f5867d216b815dd1acb1b4da2e794d1095 (diff) | |
unsafe_type_of -> get_type_of in Extractactics.mkCaseEq
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|]))]; |