coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-02-05	Unset the Ltac backtrace printing by default.	Pierre-Marie Pédrot
	This is only used for debugging, if a user wants more feedback she can turn on the option. Conversely, it has a cost for any tactic script, so it is wiser to disable it by default.
2018-09-10	Fixing an inconsistency in interpreting Ltac names linking to binder names.	Hugo Herbelin
	The recursion names in fix and cofix were not renamed like other binders were.
2018-05-17	Introduce an option to allow nested lemma, and turn it off by default.	Théo Zimmermann

2017-11-20	Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).	Hugo Herbelin
	Was broken since 8.6.
2016-10-24	Adding a test for #4398 (interpretation scopes for "match goal").	Hugo Herbelin

2016-10-22	Merge branch 'v8.5' into v8.6	Hugo Herbelin

2016-10-22	Fixing printing of generic arguments of tag "var".	Hugo Herbelin

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-04-09	A small test of Print Ltac.	Hugo Herbelin

2015-10-11	Fixing test-suite	Hugo Herbelin

2015-10-11	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin
	Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables.
2015-10-11	Refining 0c320e79ba30 in fixing interpretation of constr under binders	Hugo Herbelin
	which was broken after it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). Interpretation was corrected, but error message was damaged.