diff options
| author | Pierre-Marie Pédrot | 2016-03-17 23:49:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-18 00:26:35 +0100 |
| commit | b5f6eb57a480d705be9362067e2fb887533c822c (patch) | |
| tree | 1d5d50a20968a3fb8607ff9f15d6153dfa7f3fec /stm/asyncTaskQueue.ml | |
| parent | 36e865119e5bb5fbaed14428fc89ecd4e96fb7be (diff) | |
ARGUMENT EXTEND made of only one entry share the same grammar.
This fixes parsing conflicts with the [fix ... with] tactic.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions