The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 16 Jan 2013 11:06:06 +0200,
Dmitry Grebeniuk 
<gdsfh1 AT gmail.com>
 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.)

I think it would be a nice addition to extend the refine tactic with
some syntax to call tactics like this:

refine_with_tactics ( {| n := 7 ; n_lt_10 := <#omega#> ; b := true ;
                         b_tf := <#apply bool_tf#> |}.

So that the code between <# and #> could be solved by the provided
proof script. My suggestion or Guillaume's one work, but having a
plugin for that, so that it is internally managed would be better.

I think I will fill a feature request.