diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-02-23 18:58:43 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-02-23 18:58:43 +0100 |
| commit | cea92f33654bf924f5be861a946ee5084eca840b (patch) | |
| tree | 97a825a97dd65a4d9d74b6870cc6396a1345901b | |
| parent | df2f50db3703b4f7f88f00ac382c7f3f1efaceb3 (diff) | |
Fixed 3233 (fresh does not work with a qualid).
fresh now accepts a qualid, and behaves as if given the short name.
Since fresh used to accept an id, supporting qualid is IMO not a new
feature but just a fix. Hence the fix in v8.5.
| -rw-r--r-- | parsing/g_ltac.ml4 | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index b4d96e5cb..3cd7dbc9b 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -153,8 +153,12 @@ GEXTEND Gram | IDENT "type_term"; c=uconstr -> TacPretype c | IDENT "numgoals" -> TacNumgoals ] ] ; + (* If a qualid is given, use its short name. TODO: have the shortest + non ambiguous name where dots are replaced by "_"? Probably too + verbose most of the time. *) fresh_id: - [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ] + [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) + | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> |