diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/recdef.ml | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index a96ec6a438..25e664336c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -971,9 +971,22 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ Auto.h_auto None [] (Some []) g | _ -> incr h_num; - tclTHEN - (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) - e_assumption + (observe_tac "finishing using" + ( + tclCOMPLETE( + tclFIRST[ + tclTHEN + (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)) + e_assumption; + Eauto.eauto_with_bases + false + (true,5) + [delayed_force refl_equal] + [Auto.Hint_db.empty empty_transparent_state false] + ] + ) + ) + ) g) ; Command.save_named opacity; |