coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-08-18	Remaining bugs in PR#12223 which fixed location of tactic errors (issue #12152).	Hugo Herbelin
	The update of a loc needs sometimes to override (when calling an Ltac function), and otherwise to keep the existing loc (assumed to be fined). We refine this (see e.g. the ErrorLocation_tac_in_term tests). Moreover, when overriding, this was going to a tclOR backtracking point which was setting the loc to a completely disjoint part of the code having caused the error (see #12773). We replace the tclOR by a tclORELSE.