diff options
| author | Gaëtan Gilbert | 2020-02-06 16:10:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 1fd5cec8fbc7323ac7bd710707f37d906c5bc794 (patch) | |
| tree | 02fbaf937d58ac5454b14f139d069460b819fc28 | |
| parent | d584d0643e32f2277b1a38ba46fc92993638492b (diff) | |
unsafe_type_of -> get_type_of in Tacticals.general_elim_then_using
| -rw-r--r-- | tactics/tacticals.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ed7ab9164a..5db72e669e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -633,7 +633,7 @@ module New = struct (Proofview.Goal.enter begin fun gl -> let indclause = mk_clenv_from gl (c, t) in (* applying elimination_scheme just a little modified *) - let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim) in + let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in let indmv = match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv |