coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-11-24	Extending further PR#6047 (system to register printers for Ltac values).	Hugo Herbelin
	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.
2017-11-02	Setting a system to register printers for Ltac values.	Hugo Herbelin
	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".
2017-11-02	Using a specific function to register vernac printers.	Hugo Herbelin

2017-11-02	Exporting a few more printing functions.	Hugo Herbelin

2017-10-03	Moving the Ltac-specific part of the nametab to the Ltac plugin.	Pierre-Marie Pédrot
	For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit.
2017-09-26	Properly display the "only" prefix for selectors (bug #5760).	Guillaume Melquiond
	This commit also fixes range selectors being incorrectly displayed.
2017-08-29	A new step of restructuration of notations.	Hugo Herbelin
	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).
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-06-07	Put all plugins behind an "API".	Matej Kosik

2017-06-01	[printing] Remove duplicated printing function.	Emilio Jesus Gallego Arias
	It seems there were 4 copies of the same function in the code base.
2017-05-24	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias

2017-05-16	Adding support for using grammar entries returning no value in EXTEND.	Hugo Herbelin

2017-04-25	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias
	Now it is a private field, locations are optional.
2017-03-24	Merge branch 'trunk' into pr379	Maxime Dénès

2017-03-21	[pp] Remove unused printing tagging infrastructure.	Emilio Jesus Gallego Arias
	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.
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.