index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
class_tactics.ml
Commit message (
Expand
)
Author
Age
*
Hints API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Equality API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Clenv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Tacmach API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Refine API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Goal API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Pretyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Typeclasses API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Constr_matching API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evarconv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
*
sections/hints: prevent Not_found in get_type_of
Matthieu Sozeau
2016-10-21
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-05
|
\
|
|
*
Clean up type classes flags and update compat file.
Maxime Dénès
2016-10-05
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-02
|
\
|
|
*
Fix bug #4893: not_evar: unexpected failure in 8.5pl1.
Pierre-Marie Pédrot
2016-08-30
*
|
CLEANUP: using |> operator more consistently
Matej Kosik
2016-08-30
*
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
/
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
Typeclasses: fix treatment of exceptions in compat
Matthieu Sozeau
2016-06-27
*
Typeclasses: mark unresolvable goals in new implementation
Matthieu Sozeau
2016-06-27
*
We want tclORELSE to catch exceptions on backtrackings
Matthieu Sozeau
2016-06-27
*
Typeclasses:rename solve_instantiation* & use Hook
Matthieu Sozeau
2016-06-16
*
Fix resolve_one_typeclass to use the new engine
Matthieu Sozeau
2016-06-16
*
Bind resolve_one_typeclass to 8.5 or 8.6 resolution
Matthieu Sozeau
2016-06-16
*
Put autoapply back, lost during rebase
Matthieu Sozeau
2016-06-16
*
Cleanup and refactoring
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: allow shelved subgoals
Matthieu Sozeau
2016-06-16
*
Minor cleanup
Matthieu Sozeau
2016-06-16
*
Typeclasses: refine the eauto tactic
Matthieu Sozeau
2016-06-16
*
Typeclasses: verbosity and Limit Intros options
Matthieu Sozeau
2016-06-16
*
typeclass resolution: add two compatibility options
Matthieu Sozeau
2016-06-16
*
Fix incorrect caching of local hints w.r.t sections
Matthieu Sozeau
2016-06-16
*
Compat with ocaml 4.01
Matthieu Sozeau
2016-06-16
*
Fix iterative deepening strategy failing too early
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-16
*
Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for uniform...
Hugo Herbelin
2016-06-02
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Put the "exact" family of tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
Moving Eauto and Class_tactics to tactics/.
Pierre-Marie Pédrot
2016-03-25
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
*
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
*
|
Moving conversion functions to the new tactic API.
Pierre-Marie Pédrot
2016-02-15
[next]
Pierre-Marie Pédrot
Matthieu Sozeau
Maxime Dénès
Matej Kosik
Matej Kosik
Pierre Letouzey
Hugo Herbelin
Emilio Jesus Gallego Arias