index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
pptactic.mli
Age
Commit message (
Expand
)
Author
2019-03-20
Stop accessing proof env via Pfedit in printers
Maxime Dénès
2018-12-11
[api] Move reduction modules to `tactics`
Emilio Jesus Gallego Arias
2018-11-28
[ltac] Remove aliases already present in the lower layers.
Emilio Jesus Gallego Arias
2018-06-12
[api] Remove Misctypes.
Emilio Jesus Gallego Arias
2018-06-12
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-05-31
[notations] Split interpretation and parsing of notations
Emilio Jesus Gallego Arias
2018-05-01
[api] Move bullets and goals selectors to `proofs/`
Emilio Jesus Gallego Arias
2018-04-02
[api] Move some types to their proper module.
Emilio Jesus Gallego Arias
2018-03-10
[ssreflect] Fix module scoping problems due to packing and mli files.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-11-24
Extending further PR#6047 (system to register printers for Ltac values).
Hugo Herbelin
2017-11-02
Setting a system to register printers for Ltac values.
Hugo Herbelin
2017-11-02
Using a specific function to register vernac printers.
Hugo Herbelin
2017-11-02
Exporting a few more printing functions.
Hugo Herbelin
2017-10-03
Moving the Ltac-specific part of the nametab to the Ltac plugin.
Pierre-Marie Pédrot
2017-09-26
Properly display the "only" prefix for selectors (bug #5760).
Guillaume Melquiond
2017-08-29
A new step of restructuration of notations.
Hugo Herbelin
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-17
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-06-01
[printing] Remove duplicated printing function.
Emilio Jesus Gallego Arias
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-16
Adding support for using grammar entries returning no value in EXTEND.
Hugo Herbelin
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-21
[pp] Remove unused printing tagging infrastructure.
Emilio Jesus Gallego Arias
2017-02-17
Ltac as a plugin.
Pierre-Marie Pédrot
