The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Consider instead:

Tactic Notation "oexact'" open_constr(term) := exact term.

Tactic Notation "oexact" uconstr(term) := lazymatch goal with |- ?G => oexact' (term : G) end.

Otherwise, the following fails:

Goal 0 = 1 -> False.

  oexact (fun H => match H with eq_refl => fun p => p end).

(Note that [exact] and [refine] do bidirectional typechecking.)

On Tue, Sep 27, 2016 at 7:45 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

If you're using typeclasses, you may have run into cases where
refinement runs when you'd rather it didn't.  Here are a few very simple
tactics that can help: orefine and simple orefine, which act like refine
and simple refine, except that they don't run instance refinement in holes:

Tactic Notation "oexact" open_constr(term) := exact term.

Tactic Notation "orefine" uconstr(term) := unshelve oexact term;
shelve_unifiable.

Tactic Notation "simple" "orefine" uconstr(term) := unshelve oexact term.

(*Example:*)
Variable Foo : Type.
Existing Class Foo.
Variable Foo1 : Foo.
Goal True.
refine (let f := _ : Foo in _). (*f := Foo1 : Foo*)
orefine (let g := _ : Foo in _). (*g := ?f : Foo*)


However, beware of bug 4416...

-- Jonathan