coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-03-21	Merge PR#134: Enable `-safe-string`	Maxime Dénès

2017-03-17	Merge PR#428: Report missing tactic arguments in error message	Maxime Dénès

2017-03-17	Merge PR#445: TACTIC EXTEND now takes an optional level as argument.	Maxime Dénès

2017-03-15	Attempt to improve error message when "apply in" fail.	Hugo Herbelin
	- Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390.
2017-03-14	[safe-string] ltac/profile_ltac	Emilio Jesus Gallego Arias
	No functional change, one extra copy introduced but it seems hard to avoid.
2017-03-14	Report missing tactic arguments in error message	Tej Chajed
	Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
2017-03-14	Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun	Maxime Dénès

2017-02-27	Merge PR#395: Allow hintdb to be parameters in a Ltac definition or	Maxime Dénès
	Tactic Notation
2017-02-24	TACTIC EXTEND now takes an optional level as argument.	Maxime Dénès
	The syntax is: TACTIC EXTEND foo AT LEVEL i This commit makes it possible to define tacticals like the ssreflect arrow without having to resort to GEXTEND statements and intepretation hacks. Note that it simply makes accessible through the ML interface what Tactic Notation already supports: Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
2017-02-24	Revert "Add empty ltac_plugin file for forward compatibility."	Maxime Dénès
	This reverts commit e8137ae63b3b19436755f372b595e7343e942894, was meant for 8.6 branch only.
2017-02-22	Merge branch 'v8.6'	Pierre-Marie Pédrot

2017-02-17	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot
	This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
2017-02-17	Ltac as a plugin.	Pierre-Marie Pédrot
	This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.