index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
/
printer.ml
Commit message (
Expand
)
Author
Age
*
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
*
[printing] Deprecate all printing functions accessing the global proof.
Emilio Jesus Gallego Arias
2017-11-21
*
[proof] Attempt to deprecate some V82 parts of the proof API.
Emilio Jesus Gallego Arias
2017-11-19
*
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Finish removing Show Goal uid
Gaëtan Gilbert
2017-11-04
*
Exporting the level-parametric printer of constr and its variants.
Hugo Herbelin
2017-11-02
*
Merge PR #830: Moving assert (the "Cut" rule) to new proof engine
Maxime Dénès
2017-08-29
|
\
*
|
Printing goals does not evar-normalizes beforehand anymore.
Pierre-Marie Pédrot
2017-08-01
*
|
Detyping functions are now operating on EConstr.t.
Pierre-Marie Pédrot
2017-08-01
*
|
Merge PR #919: Remove a few useless evar-normalizations in printing code.
Maxime Dénès
2017-08-01
|
\
\
*
|
|
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
|
*
|
Remove a few useless evar-normalizations in printing code.
Pierre-Marie Pédrot
2017-07-26
|
/
/
*
|
Merge PR #770: [proof] Move bullets to their own module.
Maxime Dénès
2017-07-19
|
\
\
*
|
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
|
*
Moving "assert" (internally "Cut") to the new proof engine.
Hugo Herbelin
2017-06-25
|
|
/
|
/
|
*
|
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
|
Add printing of cumulativity in inductive types
Amin Timany
2017-06-16
*
|
Using UInfoInd for universes in inductive types
Amin Timany
2017-06-16
|
*
[proof] Move bullets to their own module.
Emilio Jesus Gallego Arias
2017-06-12
*
|
[proof] Deprecate redundant wrappers.
Emilio Jesus Gallego Arias
2017-06-11
|
/
*
[emacs] [toplevel] Make emacs flag local to the toplevel.
Emilio Jesus Gallego Arias
2017-06-01
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-25
|
\
*
\
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
|
|
*
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-05-24
|
|
/
|
*
Merge PR#457: Adding an even more compact goal hyps mode.
Maxime Dénès
2017-05-17
|
|
\
|
|
*
Simplified compaction criterion + tests.
Pierre Courtieu
2017-05-16
|
|
*
Adapted to EConstr.
Pierre Courtieu
2017-05-05
|
*
|
Warning removed.
Pierre Courtieu
2017-05-04
|
*
|
labelizing arguments
Pierre Courtieu
2017-05-04
|
*
|
Adding an option "Printing Unfocused".
Pierre Courtieu
2017-05-04
|
|
*
Adding an even more compact mode for goal display.
Pierre Courtieu
2017-05-03
|
|
/
|
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
|
/
*
Merge PR#441: Port Toplevel to the Stm API
Maxime Dénès
2017-04-12
|
\
|
*
[flags] Documentation and a minor tweak.
Emilio Jesus Gallego Arias
2017-04-12
*
|
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
|
\
|
|
*
[pp] Prepare for serialization, remove opaque glue.
Emilio Jesus Gallego Arias
2017-03-21
|
*
Fixing Bug 5383 (Hyps Limit) + small refactoring.
Pierre Courtieu
2017-03-07
*
|
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
|
\
|
*
|
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Moving printing code from Evd to Termops.
Pierre-Marie Pédrot
2017-02-14
*
|
Introducing contexts parameterized by the inner term type.
Pierre-Marie Pédrot
2017-02-14
*
|
Evar-normalizing functions now act on EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing compatibility layers related to printing.
Pierre-Marie Pédrot
2017-02-14
*
|
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Tactic_matching API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Goal API using EConstr.
Pierre-Marie Pédrot
2017-02-14
[next]