diff options
| author | Emilio Jesus Gallego Arias | 2017-05-20 02:05:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-05-20 15:03:51 +0200 |
| commit | 9452f9a3b3bee737c3b4b687e1601eb4ca45b298 (patch) | |
| tree | 9960fdd57b4b6404e616204b7095c7fbe1d02613 /API/grammar_API.ml | |
| parent | b7cf93cec115b61889e31c0abefdbd29d9b51ebe (diff) | |
[coqdoc] Add keywords in bug 2884.
Diffstat (limited to 'API/grammar_API.ml')
0 files changed, 0 insertions, 0 deletions