search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
486 stars 87 forks source link

PG does not position to error #781

Open Matafou opened 2 weeks ago

Matafou commented 2 weeks ago

This bug appeared because of PR #774. Backtracking it is not satisfying because #773 shows a good reason for it.

Example:

Require Import Utf8.
Definition trois := 3. (*test-definition*)
Definition β := 3. (*test-definition*)
Definition β' := 3. (*test-definition*)
Definition β'' := 3. (*test-definition*)
Print trois.
Eval compute in (λ γγ:nat, γγ)
                       4 +
                       (λ a:nat, a) 4
                     + ααα * trois * trois.

the error is not positioned on ααα. This has nothing to do with utf8, but any fix should check that it works ok for this.

Matafou commented 2 weeks ago

original issue by Vadim Silva on zulip.