coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-10-29	Fixing #5164 (regression in locating error in argument of "refine").	Hugo Herbelin
	Reporting location was not expecting a term passed to an ML tactic to be interpreted by the ML tactic itself. Made an empirical fix to report about the as-precise-as-possible location available.
2016-07-03	rename toplevel/cerror.ml into explainErr.ml (too close to the new ↵	Pierre Letouzey
	lib/cErrors.ml)
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey
	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-06-18	Backporting c064fb933 from 8.5 (another regression with Ltac trace report).	Hugo Herbelin
	Doing it explicitly because it is in another file.
2016-06-06	About printing of traces of failures while calling ltac code.	Hugo Herbelin
	An Ltac trace printing mechanism was introduced in 8.4 which was inadvertedly modified by a series of commits such as 8e10368c3, 91f44f1da7a, ... It was also sometimes buggy, iirc, when entering ML tactics which themselves were calling ltac code. It got really bad in 8.5 as in: Tactic Notation "f" constr(x) := apply x. Ltac g x := f x. Goal False. idtac; f I. (* bad location reporting ) g I. ( was referring to tactic name "Top.Top#<>#1" *) which this commit fixes. I don't have a clear idea of what would be the best ltac tracing mechanism, but to avoid it to be broken without being noticed, I started to add some tests. Eventually, it might be worth that an Ltac expert brainstrom on it!
2016-03-21	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot