diff options
| author | Gaëtan Gilbert | 2020-02-06 17:13:33 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 38e1e823cf5329762e97902a6ded54c95a5a5c61 (patch) | |
| tree | 2771208011ff251a875ba4db2407b7d9669a1b64 | |
| parent | 8a8217fe0b1ba8b7548ae648368774105cf21b11 (diff) | |
unsafe_type_of -> get_type_of in Leminv.lemInv
| -rw-r--r-- | tactics/leminv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index cf58c9306c..def4af1ae8 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -259,7 +259,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac = let lemInv id c = Proofview.Goal.enter begin fun gls -> try - let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in + let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false with |