aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
...
* | | 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
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 03:00:24 +0000