diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index a9b162819..e4695792b 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1143,7 +1143,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g mk_correct_id f_id in - ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ()); + (try Backtrack.reset_name (Pp.dummy_loc,first_lemma_id) with _ -> ()); raise e |