index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
tac2tactics.ml
Age
Commit message (
Expand
)
Author
2017-11-02
Binding the specialize tactic.
Pierre-Marie Pédrot
2017-10-30
Fix the semantics of introducing with empty intro patterns.
Pierre-Marie Pédrot
2017-10-30
Introducing the change tactic.
Pierre-Marie Pédrot
2017-10-30
Fix compilation after merge of Ltac_pretype interface.
Pierre-Marie Pédrot
2017-10-07
Remove unused warnings.
Pierre-Marie Pédrot
2017-10-01
Using Ltac2 native closures in some tactic APIs.
Pierre-Marie Pédrot
2017-10-01
Rolling up our own representation of clauses.
Pierre-Marie Pédrot
2017-10-01
Moving ML types used by Ltac2 to their proper interface.
Pierre-Marie Pédrot
2017-09-26
Adding quotations for the assert family of tactics.
Pierre-Marie Pédrot
2017-09-15
Making Ltac2 representation of data coincide with the ML-side one.
Pierre-Marie Pédrot
2017-09-07
Communicate the backtrace through the monad.
Pierre-Marie Pédrot
2017-09-05
Binding the firstorder tactic.
Pierre-Marie Pédrot
2017-09-05
Binding the inversion family of tactics.
Pierre-Marie Pédrot
2017-09-05
Typeclasses_eauto strategy is now optional.
Pierre-Marie Pédrot
2017-09-05
More static invariants for typeclass_eauto.
Pierre-Marie Pédrot
2017-09-05
ML bindings of auto-related tactics.
Pierre-Marie Pédrot
2017-09-04
Quick-and-dirty backtrace mechanism for the interpreter.
Pierre-Marie Pédrot
2017-08-30
Binding reduction functions acting on terms.
Pierre-Marie Pédrot
2017-08-25
More bindings to primitive tactics.
Pierre-Marie Pédrot
2017-08-24
Use references in reduction tactics.
Pierre-Marie Pédrot
2017-08-18
Removing dead code.
Pierre-Marie Pédrot
2017-08-05
Exporting more reduction functions.
Pierre-Marie Pédrot
2017-08-05
Exporting the rewrite tactic.
Pierre-Marie Pédrot
2017-08-04
Adding the induction and destruct tactics.
Pierre-Marie Pédrot
2017-08-02
Tentatively implementing apply.
Pierre-Marie Pédrot
