aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml
Commit message (Expand)AuthorAge
...
* | | | Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* | | | Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * | | Merge remote-tracking branch 'github/pr/172' into trunkGravatar Maxime Dénès2016-12-19
| |\ \ \
| * \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
| |\ \ \ \ | | | |/ / | | |/| |
| | * | | Fix shelving order in typeclasses eauto.Gravatar Théo Zimmermann2016-11-30
| | * | | Fix typeclasses eauto shelving.Gravatar Théo Zimmermann2016-11-30
| * | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/| | | | | |/ / /
| * | | Minor debug printing bug,Gravatar Matthieu Sozeau2016-11-16
| * | | Revert more of a477dc for good measureGravatar Matthieu Sozeau2016-11-16
| * | | Revert part of a477dc, disallow_shelvedGravatar Matthieu Sozeau2016-11-15
| * | | Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \ \
| * \ \ \ Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \ \ \
| * \ \ \ \ Merge remote-tracking branch 'github/pr/335' into v8.6Gravatar Maxime Dénès2016-11-04
| |\ \ \ \ \
| | | | * | | Rework search_strategy option handlingGravatar Matthieu Sozeau2016-11-03
| | | | * | | Internal API change to typeclasses eauto.Gravatar Théo Zimmermann2016-11-03
| | | | * | | Do not shelve non-class subgoals but fail, it shouldGravatar Matthieu Sozeau2016-11-03
| | | | * | | typeclasses eauto Implem/doc of shelving strategyGravatar Matthieu Sozeau2016-11-03
| | | | * | | Fix [typeclasses eauto with] and nopattern hintsGravatar Matthieu Sozeau2016-11-03
| | | | * | | Fix handling of only_classes at toplevelGravatar Matthieu Sozeau2016-11-03
| | | | * | | Handle Unique Solutions flag.Gravatar Matthieu Sozeau2016-11-03
| | | | * | | TCS: error handling and debug printing in resolutionGravatar Matthieu Sozeau2016-11-03
| | | | * | | Fix bugs in Filtered Unification and cleanup codeGravatar Matthieu Sozeau2016-11-03
| | | | * | | Fix Typeclasses eauto := bfs.Gravatar Matthieu Sozeau2016-11-03
| | | | * | | Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| | |_|/ / / | |/| | | |
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| | | | |
| | * | | | Fix printing of typeclasses eauto debug wrt intro.Gravatar Théo Zimmermann2016-10-24
| | | * | | Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | |/ / /
| * / / / sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
| |/ / /
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| | |
| * | | Clean up type classes flags and update compat file.Gravatar Maxime Dénès2016-10-05
| | | * Fix bug 4969, autoapply was not tagging shelved subgoals correctly as unresol...Gravatar Matthieu Sozeau2016-09-29
| | |/ | |/|
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| |