aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printer.ml
Commit message (Expand)AuthorAge
...
| | * Adding an even more compact mode for goal display.Gravatar Pierre Courtieu2017-05-03
| |/
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* 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-03-24
|\|
| * [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * 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
* | 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
* | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Goal 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édrot2016-11-18
|/|
| * Do not print dependent evars by default (expensive)Gravatar Matthieu Sozeau2016-11-05
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\|
| * Refine printing of pending unification constraintsGravatar Matthieu Sozeau2016-10-20
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-27
|\|
| * Moving "move" in the new proof engine.Gravatar Hugo Herbelin2016-09-24
* | 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: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* 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
* proof mode: print unification constraintsGravatar Matthieu Sozeau2016-06-16
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\ \
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * | Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
* | | Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Remove extraneous space in coqtop/pg output (bug #4675).Gravatar Guillaume Melquiond2016-05-03
* | | Merge branch 'linear-comparison' of https://github.com/aspiwack/coq into aspi...Gravatar Matthieu Sozeau2016-04-04
|\ \ \
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \ \ \ | | |/ / | |/| |
| * | | Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
* | | | Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \ \
* \ \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ \ \ | | |/ / / | |/| | |
| * | | | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
| | * | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ / / |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 15:06:40 +0000