The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 19/12/2012 18:36, Jason Gross wrote:
> Can someone explain to me why it matters whether I name a tactic [rew] or
> [rew'] in the following code (in Coq 8.4):

The tactic 'rew' is hardwired in the 'rewrite.ml4' file by the following
code:

TACTIC EXTEND GenRew
| [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at"
occurrences(occ) ] ->
    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
| [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ)
"in" hyp(id) ] ->
    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
| [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
    [ cl_rewrite_clause_newtac_tac c o all_occurrences (Some id) ]
| [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
    [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None ]
| [ "rew" orient(o) glob_constr_with_bindings(c) ] ->
    [ cl_rewrite_clause_newtac_tac c o all_occurrences None ]
END

This means that your problem lies in the parsing stratum, which is quite
annoying indeed (and can't be solved).

PMP

Attachment: signature.asc
Description: OpenPGP digital signature