aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
Commit message (Expand)AuthorAge
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* Fixing printing of Instance.Gravatar Hugo Herbelin2016-06-16
* Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
* Revert "Temporary deactivate re-interpretation of terms in beautify."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printing of Instance."Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Instance.Gravatar Hugo Herbelin2016-04-27
* Temporary deactivate re-interpretation of terms in beautify.Gravatar Hugo Herbelin2016-04-27
* A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
* Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
|/
* Improving over printing of let-tuple (see #4447).Gravatar Hugo Herbelin2015-12-03
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Add a space in cast since cast binds loosely.Gravatar Gregory Malecha2015-06-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing printing of dirpathes in Ppconstr. It was reversed.Gravatar Pierre-Marie Pédrot2014-11-30
* Adding tag output to references in Ppconstr.Gravatar Pierre-Marie Pédrot2014-11-25
* Adding notation terminals to coqtop highlight.Gravatar Pierre-Marie Pédrot2014-11-17
* Fixing semantics of Ppconstr.print_hunks.Gravatar Pierre-Marie Pédrot2014-11-17
* Missing keywords in Ppconstr.Gravatar Pierre-Marie Pédrot2014-11-17
* Moving printing code for red_expr and may_eval to Pptactic.Gravatar Pierre-Marie Pédrot2014-11-17
* Default styles for printing tags.Gravatar Pierre-Marie Pédrot2014-11-17
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Additional style tags for constrs.Gravatar Pierre-Marie Pédrot2014-11-15
* Setting a keyword tag in Ppconstr.Gravatar Pierre-Marie Pédrot2014-11-15
* Plug the dynamic tags in the Richpp mechanism.Gravatar Pierre-Marie Pédrot2014-11-10
* lib/RichPp: Rename into Richpp.Gravatar Yann Régis-Gianas2014-11-05
* lib/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
* lib/Pp.tag: New.Gravatar Regis-Gianas2014-11-04
* printing/Ppannotation: Introduce a new annotation for keywords.Gravatar Regis-Gianas2014-11-04
* Ppannotation: New.Gravatar Regis-Gianas2014-11-04
* printing/Ppconstr.Make:Gravatar Regis-Gianas2014-11-04
* printing/Ppconstr.print_hunks:Gravatar Regis-Gianas2014-11-04
* printing/Ppconstr: Cosmetics.Gravatar Regis-Gianas2014-11-04
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Printing evar instance in a more intuitive order.Gravatar Hugo Herbelin2014-09-29
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* A couple of fixes/improvements in -beautify, but backtracking onGravatar Hugo Herbelin2014-08-12
* Preliminary re-installation of notation interpretation in beautifying mode.Gravatar Hugo Herbelin2014-08-05
* Fixing a few beautifying bugs.Gravatar Hugo Herbelin2014-08-05
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* - Better parsing and printing of named universes: Type{ident} and foo@{(ident...Gravatar Matthieu Sozeau2014-06-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 18:49:28 +0000