diff options
| author | Hugo Herbelin | 2017-05-22 10:01:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 00:52:26 +0200 |
| commit | d9ea37641bc67ca269065a9489ec8e70b2f2d246 (patch) | |
| tree | d4c7c232abc82c84994979e68a518c692abd3635 /engine/ftactic.mli | |
| parent | ca630605330828b9b6456477b0fd4f8a0c3f1831 (diff) | |
Locating error about clash between a inductive parameter and a bound variable.
Also trying to reformulate the message, distinguishing between a
variable/parameter and its name.
Diffstat (limited to 'engine/ftactic.mli')
0 files changed, 0 insertions, 0 deletions