diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 43658e8021..e047f13d53 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1450,7 +1450,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = Eauto.eauto_with_bases false (true,5) - [Lazy.force refl_equal] + [Evd.empty,Lazy.force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] ) ) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 057ffb9b32..f066e39d05 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1005,7 +1005,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ Eauto.eauto_with_bases false (true,5) - [delayed_force refl_equal] + [Evd.empty,delayed_force refl_equal] [Auto.Hint_db.empty empty_transparent_state false] ] ) |