index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
tacexpr.mli
Commit message (
Expand
)
Author
Age
*
Remove reference name type.
Maxime Dénès
2018-06-18
*
[api] Remove Misctypes.
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Misctypes removal: move Tactypes to proofs
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Misctypes removal: multi to tactics/rewrite
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Move bullets and goals selectors to `proofs/`
Emilio Jesus Gallego Arias
2018-05-01
*
Strict focusing using Default Goal Selector.
Gaëtan Gilbert
2018-04-29
*
[api] Move some types to their proper module.
Emilio Jesus Gallego Arias
2018-04-02
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
Remove deprecated option Tactic Compat Context.
Théo Zimmermann
2017-12-11
*
Adding support for syntax "let _ := e in e'" in Ltac.
Hugo Herbelin
2017-11-04
*
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-10-25
*
Moving the Ltac-specific part of the nametab to the Ltac plugin.
Pierre-Marie Pédrot
2017-10-03
*
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-17
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-06-09
*
Put all plugins behind an "API".
Matej Kosik
2017-06-07
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Adding "epose", "eset", "eremember" which allow to set terms with
Hugo Herbelin
2017-05-30
*
Adding "eassert", "eenough", "epose proof", which allow to state
Hugo Herbelin
2017-05-30
*
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
*
[location] Use located in tactics.
Emilio Jesus Gallego Arias
2017-04-24
*
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
*
Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun
Maxime Dénès
2017-03-14
*
Ltac as a plugin.
Pierre-Marie Pédrot
2017-02-17