aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorHugo Herbelin2017-07-18 13:34:14 +0200
committerHugo Herbelin2017-07-18 13:38:42 +0200
commit4af1609cd70cca670109dfd6dfa06ed02034f7ae (patch)
tree4a81a8c034288099b7e2e5f41c8efbb7874156f3 /dev
parent9427b99b167842bc4a831def815c4824030d518f (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 'dev')
0 files changed, 0 insertions, 0 deletions