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
...
|
*
|
|
Revert part of a477dc, disallow_shelved
Matthieu Sozeau
2016-11-15
|
*
|
|
Merge remote-tracking branch 'github/pr/339' into v8.6
Maxime Dénès
2016-11-07
|
|
\
\
\
|
*
\
\
\
Merge commit 'e6edb33' into v8.6
Maxime Dénès
2016-11-07
|
|
\
\
\
\
|
*
\
\
\
\
Merge remote-tracking branch 'github/pr/335' into v8.6
Maxime Dénès
2016-11-04
|
|
\
\
\
\
\
|
|
|
|
*
|
|
Rework search_strategy option handling
Matthieu Sozeau
2016-11-03
|
|
|
|
*
|
|
Internal API change to typeclasses eauto.
Théo Zimmermann
2016-11-03
|
|
|
|
*
|
|
Do not shelve non-class subgoals but fail, it should
Matthieu Sozeau
2016-11-03
|
|
|
|
*
|
|
typeclasses eauto Implem/doc of shelving strategy
Matthieu Sozeau
2016-11-03
|
|
|
|
*
|
|
Fix [typeclasses eauto with] and nopattern hints
Matthieu Sozeau
2016-11-03
|
|
|
|
*
|
|
Fix handling of only_classes at toplevel
Matthieu Sozeau
2016-11-03
|
|
|
|
*
|
|
Handle Unique Solutions flag.
Matthieu Sozeau
2016-11-03
|
|
|
|
*
|
|
TCS: error handling and debug printing in resolution
Matthieu Sozeau
2016-11-03
|
|
|
|
*
|
|
Fix bugs in Filtered Unification and cleanup code
Matthieu Sozeau
2016-11-03
|
|
|
|
*
|
|
Fix Typeclasses eauto := bfs.
Matthieu Sozeau
2016-11-03
|
|
|
|
*
|
|
Lets Hints/Instances take an optional pattern
Matthieu Sozeau
2016-11-03
|
|
|
_
|
/
/
/
|
|
/
|
|
|
|
*
|
|
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
|
|
|
|
|
*
|
|
|
Fix printing of typeclasses eauto debug wrt intro.
Théo Zimmermann
2016-10-24
|
|
|
*
|
|
Renamings to avoid confusion deprecating old names
Matthieu Sozeau
2016-10-22
|
|
|
/
/
/
|
*
/
/
/
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
|
|
|
*
Fix bug 4969, autoapply was not tagging shelved subgoals correctly as unresol...
Matthieu Sozeau
2016-09-29
|
|
|
/
|
|
/
|
*
|
|
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
[prev]
[next]
Matthieu Sozeau
Maxime Dénès
Théo Zimmermann
Pierre-Marie Pédrot
Matej Kosik
Matej Kosik
Pierre Letouzey
Hugo Herbelin
Emilio Jesus Gallego Arias