aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/genprint.mli
Commit message (Collapse)AuthorAge
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
| | | | | | | | Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Extending further PR#6047 (system to register printers for Ltac values).Gravatar Hugo Herbelin2017-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.Gravatar Hugo Herbelin2017-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.Gravatar Hugo Herbelin2017-11-02
|
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Unplugging Pptactic from Ppvernac.Gravatar Pierre-Marie Pédrot2016-09-08
|
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 02:43:06 +0000