coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Ltac uses the new generic locatable API.	Pierre-Marie Pédrot	2017-10-03
\|
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
\| \| \| \| \| \| \| \| \| \| \| \|	This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
\|
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Adding support for using grammar entries returning no value in EXTEND.	Hugo Herbelin	2017-05-16
\| \|
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/ \| \| \|	Now it is a private field, locations are optional.
*	TACTIC EXTEND now takes an optional level as argument.	Maxime Dénès	2017-02-24
\| \| \| \| \| \| \| \| \| \| \| \| \|	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) := ...
*	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
	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.