The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

Hello.

> (1) This is really cool. I was hoping there was a way to extend refine's
> ability to "fill in the missing parts"

  What do you mean?  Give an example of building a term with "refine"
first, so people can help you.

> (2) This also only works on _goals_ right? Since "refine" is a generalized
> apply, I can't use this technique to rewrite an existing hypothesis (rather
> than a goal).

  You can do it.

Goal forall A (P : A -> Prop) (a : A) (H : P a) b (E : a = b), P b.
intros.
refine (let H0 := eq_ind _ _ H _ E in _).
exact H0.

(note that last two lines can be replaced with
refine (let H0 := eq_ind _ _ H _ E in H0).
)

  Generally, "refine (let H ...)" adds hypothesis H.
You can fill the body of H with "let H := thebody in ..." or leave it
empty just specifying the type with "let H : thetype := _ in ...",
then you will be prompted to build a value of thetype and the value
will be available as "H" later.