diff options
| author | Hugo Herbelin | 2017-07-18 13:34:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-07-18 13:38:42 +0200 |
| commit | 4af1609cd70cca670109dfd6dfa06ed02034f7ae (patch) | |
| tree | 4a81a8c034288099b7e2e5f41c8efbb7874156f3 /stm/asyncTaskQueue.ml | |
| parent | 9427b99b167842bc4a831def815c4824030d518f (diff) | |
Fixing a little location bug with recursive binders.
Note that localisation cannot be perfect anyways, as in the following
example, where there is no way to highlight in the original input a
syntactically stand-alone subterm where the error occurs.
> Check forall (y:nat) (x:=0), y.
> ^^^^^^^^^^^^^^^^^^^^^^^^
Error: In environment
y : nat
The term "let x := 0 in y" has type "nat" which should be Set, Prop or Type.
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions
