diff options
| author | Hugo Herbelin | 2015-02-21 13:29:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-21 13:29:58 +0100 |
| commit | dd56cc810971c407b2aecfffc82de7fc4332320a (patch) | |
| tree | 1f04f8fe4b60b0611ee68748d19460a984b51a8e /interp/constrextern.ml | |
| parent | 60411f0438740ffd8c6fc5b78875f41b3c5705ae (diff) | |
Better English for #4070 implicit arguments message (thanks to Jason for his help).
Diffstat (limited to 'interp/constrextern.ml')
0 files changed, 0 insertions, 0 deletions