aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-18
|\
| * [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Fixing a few confusions on the name of the beautify flag.Gravatar Hugo Herbelin2016-10-12
| * Moving Pp.comments to CLexer so that Pp is purer (no more side-effectGravatar Hugo Herbelin2016-10-09
| * Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * Fixing a beautifier bug pointed out by Emilio.Gravatar Hugo Herbelin2016-10-05
| * Merge remote-tracking branch 'github/pr/305' into v8.6Gravatar Maxime Dénès2016-10-04
| |\
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| |
| * | Fix bug #4661: Cannot mask the absolute name.Gravatar Pierre-Marie Pédrot2016-10-01
| | * Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
| |/
| * Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
| |\
| * | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
| * | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
| | * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
| |/
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\|
| * Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | Merge remote-tracking branch 'github/pr/283' into trunkGravatar Maxime Dénès2016-09-22
|\ \
* | | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| * | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
|/ /
| * Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* | Made Ppanotation Ltac-agnostic.Gravatar Pierre-Marie Pédrot2016-09-15
* | Moving Ltac printers to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-15
| * Fix bug #4940: Tactic notation printing could be more informative.Gravatar Pierre-Marie Pédrot2016-09-09
* | Unplugging Pptactic from Ppvernac.Gravatar Pierre-Marie Pédrot2016-09-08
* | Making Vernacexpr independent from Tacexpr.Gravatar Pierre-Marie Pédrot2016-09-08
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\ \ \ | | |/ | |/|
* | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
| * | Fix tagging of notations.Gravatar Pierre-Marie Pédrot2016-08-29
| * | Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
* | | CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, which...Gravatar Matej Kosik2016-08-26
* | | CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"Gravatar Matej Kosik2016-08-26
* | | CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
* | | CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeGravatar Matej Kosik2016-08-25
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
|/ /
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Complementing previous commit on fixes for printing binding patterns.Gravatar Hugo Herbelin2016-07-19
* Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
* Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
* Fixing missing parentheses in printing of patterns in binders.Gravatar Hugo Herbelin2016-07-19
* primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 00:18:39 +0000