diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 7 |
2 files changed, 4 insertions, 5 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index a9b1628190..e4695792be 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 diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 872d3be4ac..7613c6765f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1471,6 +1471,7 @@ let (com_eqn : int -> identifier -> let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = + let previous_label = Lib.current_command_label () in let function_type = interp_constr Evd.empty (Global.env()) type_of_f in let env = push_named (function_name,None,function_type) (Global.env()) in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) @@ -1522,7 +1523,6 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e) else anomaly "Cannot create equation Lemma" ; -(* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *) true end in @@ -1554,9 +1554,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num hook with e -> begin - ignore(try Vernacentries.vernac_reset_name (Pp.dummy_loc,functional_id) with _ -> ()); -(* anomaly "Cannot create termination Lemma" *) + (try ignore (Backtrack.backto previous_label) with _ -> ()); + (* anomaly "Cannot create termination Lemma" *) raise e end - |