diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-22 21:09:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-13 12:19:23 +0200 |
| commit | e3a3b4bb17c40b6af2ef8501c405f0600cc6d65b (patch) | |
| tree | d038fd28fc8ea222557ce492998a27a723371e04 /test-suite/success/hintdb_in_ltac.v | |
| parent | ba88e99d37817cd3a591b14bbceb61e28f3e3382 (diff) | |
Typo in a comment of plugin Quote.
Diffstat (limited to 'test-suite/success/hintdb_in_ltac.v')
0 files changed, 0 insertions, 0 deletions