index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
ltac
/
coretactics.ml4
Age
Commit message (
Expand
)
Author
2017-02-17
Ltac as a plugin.
Pierre-Marie Pédrot
2016-10-08
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-08
Fix bug #5098: Symmetry broken in HoTT.
Pierre-Marie Pédrot
2016-09-21
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-06-18
Adding an "as" clause to specialize.
Hugo Herbelin
2016-06-18
Adding eintros to respect the e- prefix policy.
Hugo Herbelin
2016-06-03
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-05-17
Put the "move" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
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-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
