index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
/
extratactics.ml4
Commit message (
Expand
)
Author
Age
*
Adding eintros to respect the e- prefix policy.
Hugo Herbelin
2016-06-18
*
Purely refactoring and code/API cleanup.
Matthieu Sozeau
2016-06-16
*
Merge PR #195: Complete is_* family of term-examining tactics.
Pierre-Marie Pédrot
2016-06-16
|
\
|
*
Add is_const
Jason Gross
2016-06-16
|
*
Add is_ind, is_constructor, is_proj
Jason Gross
2016-06-07
*
|
STM: proof block detection/error resilience API
Enrico Tassi
2016-06-06
|
/
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Put the "specialize_eq" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "generalize" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Removing useless generic arguments.
Pierre-Marie Pédrot
2016-05-04
*
More toplevel value representation sharing.
Pierre-Marie Pédrot
2016-05-04
*
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
Removing redundant *_TYPED AS clauses in EXTEND statements.
Pierre-Marie Pédrot
2016-04-12
*
Making Autorewrite independent from Ltac.
Pierre-Marie Pédrot
2016-03-25
*
Moving type_uconstr to Pretyping.
Pierre-Marie Pédrot
2016-03-25
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21