index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
/
tauto.ml
Commit message (
Expand
)
Author
Age
*
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Hipattern API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
A stronger invariant on the syntax of TacAssert, what allows for a
Hugo Herbelin
2016-06-16
*
Put the "clear" tactic into the monad.
Pierre-Marie Pédrot
2016-05-16
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Do not generate generic arguments for data which only requires toplevel values.
Pierre-Marie Pédrot
2016-05-04
*
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
Switching to an untyped toplevel representation for Ltac values.
Pierre-Marie Pédrot
2016-05-04
*
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
Hugo Herbelin
2016-04-27
*
In the short term, stronger invariant on the syntax of TacAssert, what
Hugo Herbelin
2016-04-27
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
Pierre-Marie Pédrot
Hugo Herbelin