coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Extending further PR#6047 (system to register printers for Ltac values).	Hugo Herbelin	2017-11-24
\| \| \| \| \| \| \|	We generalize the possible use of levels to raw and glob printers. This is potentially useful for printing ltac expressions which are the glob level.
*	Setting a system to register printers for Ltac values.	Hugo Herbelin	2017-11-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The model provides three kinds of printers depending on whether the printer needs a context, and, if yes if it supports levels. In the latter case, it takes defaults levels for printing when in a surrounded context (lconstr style) and for printing when not in a surrounded context (constr style). This model preserves the 8.7 focussing semantics of "idtac" (i.e. focussing only when an env is needed) but it also shows that the semantics of "idtac", which focusses the goal depending on the type of its arguments, is a bit ad hoc to understand. See discussion at PR#6047 "https://github.com/coq/coq/pull/6047#discussion_r148278454".
*	Using a specific function to register vernac printers.	Hugo Herbelin	2017-11-02
\|
*	Exporting a few more printing functions.	Hugo Herbelin	2017-11-02
\|
*	Moving the Ltac-specific part of the nametab to the Ltac plugin.	Pierre-Marie Pédrot	2017-10-03
\| \| \| \| \|	For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit.
*	Properly display the "only" prefix for selectors (bug #5760).	Guillaume Melquiond	2017-09-26
\| \| \| \|	This commit also fixes range selectors being incorrectly displayed.
*	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
\| \| \| \| \| \| \|	This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20).
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\|
*	[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
\|
*	[printing] Remove duplicated printing function.	Emilio Jesus Gallego Arias	2017-06-01
\| \| \| \|	It seems there were 4 copies of the same function in the code base.
*	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.
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|
*	[pp] Remove unused printing tagging infrastructure.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Applications of it were not clear/unproven, it made printers more complex (as they needed to be functors) and as it lacked examples it confused some people. The printers now tag unconditionally, it is up to the backends to interpreted the tags. Tagging (and indeed the notion of rich document) should be reworked in a follow-up patch, so they are in sync, but this is a first step. Tested, test-suite passes. Notes: - We remove the `Richprinter` module. It was only used in the `annotate` IDE protocol call, its output was identical to the normal printer (or even inconsistent if taggers were not kept manually in sync). - Note that Richpp didn't need a single change. In particular, its main API entry point `Richpp.rich_pp` is not used by anyone.
*	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.