aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Merge PR#552: Miscelaneous commitsGravatar Maxime Dénès2017-04-24
|\
* | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| * refactoring "Ppvernac.pr_extend"Gravatar Matej Kosik2017-04-20
|/
* Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\
| * [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\|
| * Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
| |\
| * | Fix higher-order pattern variables not being printed as "@?" (bug #5431).Gravatar Guillaume Melquiond2017-04-02
| * | Merge PR#511: [stm] Remove some obsolete vernacs/classification.Gravatar Maxime Dénès2017-03-30
| |\ \
| * | | Do so that "About" tells if a reference is a coercion.Gravatar Hugo Herbelin2017-03-27
* | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\| | |
| | * | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| |/ /
| | * Applying same convention as in Definition for printing type in a let in.Gravatar Hugo Herbelin2017-03-24
| | * Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | * Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | * Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | * "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
| |/
| * [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
| * [pp] Remove unused printing tagging infrastructure.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
| * Fixing Bug 5383 (Hyps Limit) + small refactoring.Gravatar Pierre Courtieu2017-03-07
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
| |\
| | * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2017-01-23
| | |\
| | | * Fixing a little bug in printing cofix with no arguments.Gravatar Hugo Herbelin2017-01-05
| * | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
| |\| |
| | * | Fixing printing of "ltac:" in tactics after surrounding parenthesesGravatar Hugo Herbelin2016-12-02
| | * | Fixing printing of "Set Warnings Append".Gravatar Hugo Herbelin2016-12-02
| | * | Fixing space in printing "Context".Gravatar Hugo Herbelin2016-12-02
| | * | Fixing space in printing several list of implicit arguments.Gravatar Hugo Herbelin2016-12-02
| | * | Fixing printing of "only parsing" in abbreviations.Gravatar Hugo Herbelin2016-12-02
| | * | Protect printing of ltac's "context [...]" from possible collisionGravatar Hugo Herbelin2016-12-02
| | * | More on fixing #5098 (preserving printing of "in hyp").Gravatar Hugo Herbelin2016-12-02
| | * | Properly parenthesize "ltac:" arguments (bug #5169).Gravatar Guillaume Melquiond2016-11-22
| * | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/| | | | |/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 06:25:40 +0000