index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
class_tactics.mli
Age
Commit message (
Expand
)
Author
2016-11-03
Rework search_strategy option handling
Matthieu Sozeau
2016-11-03
Internal API change to typeclasses eauto.
Théo Zimmermann
2016-11-03
Fix handling of only_classes at toplevel
Matthieu Sozeau
2016-11-03
Fix Typeclasses eauto := bfs.
Matthieu Sozeau
2016-06-16
Typeclasses:rename solve_instantiation* & use Hook
Matthieu Sozeau
2016-06-16
Purely refactoring and code/API cleanup.
Matthieu Sozeau
2016-06-16
bteauto: a Proofview.tactic for multiple goals
Matthieu Sozeau
2016-06-16
Typeclasses: refine the eauto tactic
Matthieu Sozeau
2016-06-16
Implement limited proof search and iterative deepening.
Matthieu Sozeau
2016-06-16
Typeclasses eauto based on new proof engine,
Matthieu Sozeau
2016-06-09
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-03-25
Moving Eauto and Class_tactics to tactics/.
Pierre-Marie Pédrot
2016-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2014-10-07
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2013-11-02
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-10-04
Splitting Class_tactics between code and CAMLP4/5 declarations.
ppedrot
