The Coq mailing list

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

Le Wed, 16 Jan 2013 13:42:41 +0200,
Dmitry Grebeniuk 
<gdsfh1 AT gmail.com>
 a écrit :

> Hello.
> 
>   Thank you, it's good idea too, now I have a choice
> between holes-as-inductive-type and holes-as-strings.

I think strings are more convenient as it can be used dynamically (ie.
you do not have to define an inductive). Although if your marks will be
used in many places, and you want to bind tactics to markers, then I
would recommand use of inductives (or records if you prefer, that's the
same), since it is not typing error prone (ie. if you write "makrer"
instead of "marker", as "makrer" is not a known symbol, an error will
be reported, whereas as all strings are valid, it will silently be
ignored [ie. trigger the "| _ => idtac" case]).

The syntax with "for … using …" that mimics what you wanted can also be
mixed with the strings suggestion of Guillaume, so that you will get
exactly what you asked (well, you would have to double quote your
"?mark?" and Open Scope String. I do not know if my "using" can be
replaced by your ":", but if so, you will get almost the syntax you
wanted).

With that, you wouldn't have to register marks, just to define my
"solve_extend" tactic and its associated notations once and for all,
then you have your wanted special 'refine' tactic by declaring a new
tactic notation which combines the refine tactic with my previous
notation for 'solve_extend'.