coq - The formal proof system

Age	Commit message (Collapse)	Author
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-03-03	[ltac] Move dummy plugin to plugins folder.	Emilio Jesus Gallego Arias
	This is needed to fix `Declare ML Module "ltac_plugin".
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.