index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
tacexpr.mli
Age
Commit message (
Expand
)
Author
2017-12-11
Remove deprecated option Tactic Compat Context.
Théo Zimmermann
2017-11-04
Adding support for syntax "let _ := e in e'" in Ltac.
Hugo Herbelin
2017-10-25
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-10-03
Moving the Ltac-specific part of the nametab to the Ltac plugin.
Pierre-Marie Pédrot
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-09
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-05-30
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-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-24
[location] Use located in tactics.
Emilio Jesus Gallego Arias
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-14
Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun
Maxime Dénès
2017-02-17
Ltac as a plugin.
Pierre-Marie Pédrot
