index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
rewrite.mli
Age
Commit message (
Expand
)
Author
2020-10-29
Fixing interpretation of rewrite_strat argument in Ltac.
Hugo Herbelin
2020-06-26
[declare] Move proof information to declare.
Emilio Jesus Gallego Arias
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-09
[proof] Move proofs that have an associated constant to `Lemmas`
Emilio Jesus Gallego Arias
2019-06-04
[rewrite] Add Morphism syntax made different for module type parameters
Enrico Tassi
2019-06-04
Rename Proof_global.{pstate -> t}
Gaëtan Gilbert
2019-06-04
coqpp: add new ![] specifiers for structured proof interaction
Gaëtan Gilbert
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-03-27
[coqpp] [ltac] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2018-11-28
[ltac] Remove aliases already present in the lower layers.
Emilio Jesus Gallego Arias
2018-11-02
rewrite: attributes handle is_univ_poly, is_program_mode
Gaëtan Gilbert
2018-06-12
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-11-22
[plugin] Remove LocalityFixme über hack.
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-09-28
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
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-10
Remove (useless) aliases from the API.
Matej Košík
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-04
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
Renaming local_binder into local_binder_expr.
Hugo Herbelin
2017-02-17
Ltac as a plugin.
Pierre-Marie Pédrot
