aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* 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
|\
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| * Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-19
|/
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Print the type-in-type flag in various user-facing functions.Gravatar Pierre-Marie Pédrot2016-06-18
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* proof mode: print unification constraintsGravatar Matthieu Sozeau2016-06-16
* Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
* Isolating and exporting a function for printing body of a recursive definition.Gravatar Hugo Herbelin2016-06-16
* Simplification in ppvernac.ml.Gravatar Hugo Herbelin2016-06-16
* Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Gravatar Hugo Herbelin2016-06-16
* Fixing extra space in printing bullets.Gravatar Hugo Herbelin2016-06-16
* Fixing space in printing <+ and <: + fixing missing Inline keyword.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Instance.Gravatar Hugo Herbelin2016-06-16
* Fixing extra space in printing abbreviations (SyntaxDefinition).Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Polymorphic/Monomorphic.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Arguments.Gravatar Hugo Herbelin2016-06-16
* Printing notations as parsed.Gravatar Hugo Herbelin2016-06-16
* So as to beautify to work, do not use notations in Inductive typesGravatar Hugo Herbelin2016-06-16
* Fixing missing substitution / printing cases of TacSelect.Gravatar Pierre-Marie Pédrot2016-06-16
* Fixing printing of keeping hyp on the fly.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of inversion as.Gravatar Hugo Herbelin2016-06-16
* Fixing extra space in printing destruct/induction as.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of induction/destruct as.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-06-16
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 23:27:39 +0000