index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
g_class.mlg
Age
Commit message (
Expand
)
Author
2020-11-20
Use nat_or_var where negative values don't make sense
Jim Fehrle
2020-10-19
Merge PR #13197: Require at least one reference for Typeclasses Opaque/Transp...
coqbot-app[bot]
2020-10-16
Merge PR #13195: Add support for "typeclasses eauto bfs <int_or_var_opt>"
Pierre-Marie Pédrot
2020-10-15
Require at least one reference for Typeclasses Opaque/Transparent
Jim Fehrle
2020-10-14
For "Typeclasses eauto", search depth should be a natural, not an
Jim Fehrle
2020-10-14
Add support for "typeclasses eauto bfs <int_or_var_opt>
Jim Fehrle
2020-09-11
[refman] Rename int to integer
Pierre Roux
2020-05-14
[exn] [tactics] improve backtraces on monadic errors
Emilio Jesus Gallego Arias
2020-05-06
Documenting plugin/tactic/stdlib keywords in corresponding chapters.
Hugo Herbelin
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-03-26
Declare initial hint databases in prelude
Maxime Dénès
2019-02-28
Fix #7632: Change syntax of autoapply according to the documentation.
Théo Zimmermann
2018-10-15
Port remaining EXTEND ml4 files to coqpp.
Pierre-Marie Pédrot
