diff options
| author | Pierre Courtieu | 2014-07-31 20:51:48 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2014-07-31 20:58:34 +0200 |
| commit | 04b28b0c95f15fedb2e5eef26cd87b97b4e2120d (patch) | |
| tree | 70eeda29cad0dddb6191ba5ed71dbc0a39c6d2b0 /kernel/constr.ml | |
| parent | e4cc086eb69a10ad3360333c2c83f4a59a44c416 (diff) | |
Making the error message about bullets more precise.
Suggests in some cases the right bullet to use.
Diffstat (limited to 'kernel/constr.ml')
0 files changed, 0 insertions, 0 deletions