diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-22 10:01:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 00:52:26 +0200 |
| commit | d9ea37641bc67ca269065a9489ec8e70b2f2d246 (patch) | |
| tree | d4c7c232abc82c84994979e68a518c692abd3635 /engine/eConstr.ml | |
| 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/eConstr.ml')
0 files changed, 0 insertions, 0 deletions