diff options
| author | Pierre-Marie Pédrot | 2016-05-10 11:11:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-10 19:28:24 +0200 |
| commit | 61f79019be6082c3ebabd503c322fb2edb05a99a (patch) | |
| tree | 646aaa9d5fbf289354f86f2b912a234fca7b6c20 /ltac | |
| parent | 946a3d4a800ae1f459cb67cc15c9e6ec44fb3f94 (diff) | |
AlistNsep token now accepts an arbitrary separator.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index d0383ffbcb..f829ae4f57 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -139,10 +139,10 @@ let rec prod_item_of_symbol lev = function EntryName (Rawwit (ListArg typ), Alist0 e) | Extend.Ulist1sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist1sep (e, sep)) + EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep))) | Extend.Ulist0sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist0sep (e, sep)) + EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep))) | Extend.Uopt s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in EntryName (Rawwit (OptArg typ), Aopt e) |