aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
...
* | | | Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Patternops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Find_subterm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * | | Proofview: tclINDEPENDENTLGravatar Enrico Tassi2017-02-10
| * | | Fixing injection in the presence of let-in in constructors.Gravatar Hugo Herbelin2016-12-22
| * | | 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
| |\ \ \ \ | | | |/ / | | |/| |
| | * | | Merge remote-tracking branch 'github/pr/381' into v8.6Gravatar Maxime Dénès2016-12-02
| | |\ \ \
| | | * | | Fix shelving order in typeclasses eauto.Gravatar Théo Zimmermann2016-11-30
| | | * | | Fix typeclasses eauto shelving.Gravatar Théo Zimmermann2016-11-30
| | * | | | Fix bug #5232: proper globalization of hints pathsGravatar Matthieu Sozeau2016-11-30
| | |/ / /
| * | | | Tests for info/debug auto/eauto.Gravatar Hugo Herbelin2016-11-19
| * | | | 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
| |\ \ \
| | * | | Fixes to compile with ocaml 4.01Gravatar Matthieu Sozeau2016-11-07
| * | | | Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \ \ \
| | * | | | More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
| * | | | | More precise refine compatibilityGravatar Matthieu Sozeau2016-11-05
| * | | | | Fix #3441 Use pf_get_type_of to avoid blowupGravatar Matthieu Sozeau2016-11-04
| * | | | | Fix refine in compatibility modeGravatar Matthieu Sozeau2016-11-04
| * | | | | Merge remote-tracking branch 'github/pr/335' into v8.6Gravatar Maxime Dénès2016-11-04
| |\ \ \ \ \
| * \ \ \ \ \ Merge remote-tracking branch 'github/pr/336' 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
|\| | | | | | |
| | | | | * | | Documenting changes in typeclassesGravatar Matthieu Sozeau2016-10-29
| | |_|_|/ / / | |/| | | | |
| * | | | | | Merge remote-tracking branch 'github/pr/321' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ \ \ \ \
| * | | | | | | Using msg_info for info_auto and info_eauto (PR #324).Gravatar Hugo Herbelin2016-10-26
| * | | | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\ \ \ \ \ \ \