The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le mercredi 16 janvier 2013 à 11:06 +0200, Dmitry Grebeniuk a écrit :

> So I want something like this pseudocode:
> 
> Goal myrec.
> refine ( {| n := 7 ; n_lt_10 := ?goal_nat? ; b := true ; b_tf :=
> ?goal_bool? |} ).
> for ?goal_nat? : omega.
> for ?goal_bool? : apply bool_tf.
> Qed.
> 
> (of course I understand that solution may be not so pretty as
> the pseudocode, but aesthetics is not a my target.)

Here is a small suggestion, by adding meaningless arguments.

Require Import String.

Definition named (A : Type) (s : string) := A.
Notation _as s := (_ : named _ s).

Goal myrec.
refine ( {| n := 7 ; n_lt_10 := _as "goal_nat" ; b := true ; b_tf := _as 
"goal_bool" |} ).
match goal with
| |- named _ "goal_nat" => unfold named ; omega
| |- named _ "goal_bool" => unfold named ; apply bool_tf
| _ => idtac
end.

Best regards,

Guillaume