index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
/
coretactics.ml4
Commit message (
Expand
)
Author
Age
*
Adding an "as" clause to specialize.
Hugo Herbelin
2016-06-18
*
Adding eintros to respect the e- prefix policy.
Hugo Herbelin
2016-06-18
*
Removing "rename" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "exact" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "intro" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "double induction" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Put the "move" tactic in the monad.
Pierre-Marie Pédrot
2016-05-17
*
Put the "generalize dependent" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "cofix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "*_cast_no_check" tactics in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "exact" family of tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Put the "fix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-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
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
Hugo Herbelin
Pierre-Marie Pédrot