From 28d4740736e5ef3b6f8547710dcf7e5b4d11cabd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Dec 2015 19:57:14 +0100 Subject: Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr. --- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/recdef.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f57f12f667..1474f1e936 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1473,7 +1473,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = tclCOMPLETE( Eauto.eauto_with_bases (true,5) - [Evd.empty,Lazy.force refl_equal] + [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}] [Hints.Hint_db.empty empty_transparent_state false] ) ) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5a30da336e..10a145e036 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1335,7 +1335,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp (Proofview.V82.of_tactic e_assumption); Eauto.eauto_with_bases (true,5) - [Evd.empty,Lazy.force refl_equal] + [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}] [Hints.Hint_db.empty empty_transparent_state false] ] ) -- cgit v1.2.3