aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
| |\ \ \ \ \ \
| | * \ \ \ \ \ Merge remote-tracking branch 'github/pr/338' into v8.5Gravatar Maxime Dénès2016-10-25
| | |\ \ \ \ \ \
| | | * | | | | | Remove warning now that info_auto is fixed.Gravatar Théo Zimmermann2016-10-25
| | | | | * | | | Remove v62 from the codebase.Gravatar Théo Zimmermann2016-10-25
| | |_|_|/ / / / | |/| | | | | |
| | * | | | | | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Gravatar Maxime Dénès2016-10-25
| | |/ / / / /
| | | | * / / Fix printing of typeclasses eauto debug wrt intro.Gravatar Théo Zimmermann2016-10-24
| | |_|/ / / | |/| | | |
| | * | | | Fixing printing of generic arguments of tag "var".Gravatar Hugo Herbelin2016-10-22
| | | | * | 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-17
|\| | |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
| |\| |
| | * | Still a problem with debug auto printing.Gravatar Hugo Herbelin2016-10-15
| | * | One more little bug in the output of "debug auto".Gravatar Hugo Herbelin2016-10-15