aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/genprint.ml
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
|
* Removing the untyped representation of genargs.Gravatar Pierre-Marie Pédrot2016-03-19
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
| | | | | Instead of having a version of unpackers for each level, we use a dummy argument to force unification of types.
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
|
* 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 07:29:25 +0000