index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
g_ltac.ml4
Age
Commit message (
Expand
)
Author
2018-01-05
Brackets support single numbered goal selectors.
Théo Zimmermann
2017-12-11
Remove deprecated appcontext and corresponding documentation.
Théo Zimmermann
2017-12-11
Remove deprecated option Tactic Compat Context.
Théo Zimmermann
2017-12-09
[stm] Remove all but one use of VtUnknown.
Emilio Jesus Gallego Arias
2017-11-22
[plugin] Remove LocalityFixme über hack.
Emilio Jesus Gallego Arias
2017-11-04
Adding support for syntax "let _ := e in e'" in Ltac.
Hugo Herbelin
2017-10-10
[vernac] Remove "Proof using" hacks from parser.
Emilio Jesus Gallego Arias
2017-10-03
Ltac uses the new generic locatable API.
Pierre-Marie Pédrot
2017-09-26
Properly display the "only" prefix for selectors (bug #5760).
Guillaume Melquiond
2017-07-25
[api] Remove type equalities from API.
Emilio Jesus Gallego Arias
2017-07-19
Merge PR #770: [proof] Move bullets to their own module.
Maxime Dénès
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-12
[proof] Move bullets to their own module.
Emilio Jesus Gallego Arias
2017-06-10
Remove (useless) aliases from the API.
Matej Košík
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-05-25
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-24
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-16
Adding support for using grammar entries returning no value in EXTEND.
Hugo Herbelin
2017-04-25
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-24
[location] Use located in tactics.
Emilio Jesus Gallego Arias
2017-04-24
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-21
Remove VernacError
Gaetan Gilbert
2017-04-07
[camlpX] Remove camlp4 compat layer.
Emilio Jesus Gallego Arias
2017-04-01
Declaring ltac plugin, so that static linking works.
Hugo Herbelin
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
