diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
3 files changed, 5 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ad18ea95a4..4eab5f9126 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1472,7 +1472,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/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 045beb37cf..cba10ca09d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -55,7 +55,9 @@ let pr_with_bindings_typed prc prlc (c,bl) = let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () - | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it) + | Some b -> + let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in + spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b) ARGUMENT EXTEND fun_ind_using 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] ] ) |