Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Attempt to improve error message when "apply in" fail. | 2017-03-15 | |
* | Proofview: tclINDEPENDENTL | 2017-02-10 | |
* | Fixing injection in the presence of let-in in constructors. | 2016-12-22 | |
* | Merge remote-tracking branch 'github/pr/172' into trunk | 2016-12-19 | |
|\ | |||
* \ | Merge branch 'v8.6' | 2016-12-07 | |
|\ \ | |||
| * \ | Merge remote-tracking branch 'github/pr/381' into v8.6 | 2016-12-02 | |
| |\ \ | |||
| | * | | Fix shelving order in typeclasses eauto. | 2016-11-30 | |
| | * | | Fix typeclasses eauto shelving. | 2016-11-30 | |
| * | | | Fix bug #5232: proper globalization of hints paths | 2016-11-30 | |
| |/ / | |||
* | | | Tests for info/debug auto/eauto. | 2016-11-19 | |
* | | | Merge branch 'v8.6' | 2016-11-18 | |
|\| | | |||
| * | | Minor debug printing bug, | 2016-11-16 | |
| * | | Revert more of a477dc for good measure | 2016-11-16 | |
| * | | Revert part of a477dc, disallow_shelved | 2016-11-15 | |
| * | | Merge remote-tracking branch 'github/pr/339' into v8.6 | 2016-11-07 | |
| |\ \ | |||
| | * | | Fixes to compile with ocaml 4.01 | 2016-11-07 | |
| * | | | Merge commit 'e6edb33' into v8.6 | 2016-11-07 | |
| |\ \ \ | |||
| | * | | | More explicit name for status of unification constraints. | 2016-11-07 | |
| * | | | | More precise refine compatibility | 2016-11-05 | |
| * | | | | Fix #3441 Use pf_get_type_of to avoid blowup | 2016-11-04 | |
| * | | | | Fix refine in compatibility mode | 2016-11-04 | |
| * | | | | Merge remote-tracking branch 'github/pr/335' into v8.6 | 2016-11-04 | |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge remote-tracking branch 'github/pr/336' into v8.6 | 2016-11-04 | |
| |\ \ \ \ \ | |||
| | | | | * | | Rework search_strategy option handling | 2016-11-03 | |
| | | | | * | | Internal API change to typeclasses eauto. | 2016-11-03 | |
| | | | | * | | Do not shelve non-class subgoals but fail, it should | 2016-11-03 | |
| | | | | * | | typeclasses eauto Implem/doc of shelving strategy | 2016-11-03 | |
| | | | | * | | Fix [typeclasses eauto with] and nopattern hints | 2016-11-03 | |
| | | | | * | | Fix handling of only_classes at toplevel | 2016-11-03 | |
| | | | | * | | Handle Unique Solutions flag. | 2016-11-03 | |
| | | | | * | | TCS: error handling and debug printing in resolution | 2016-11-03 | |
| | | | | * | | Fix bugs in Filtered Unification and cleanup code | 2016-11-03 | |
| | | | | * | | Fix Typeclasses eauto := bfs. | 2016-11-03 | |
| | | | | * | | Lets Hints/Instances take an optional pattern | 2016-11-03 | |
* | | | | | | | Merge branch 'v8.6' | 2016-10-29 | |
|\| | | | | | | |||
| | | | | * | | Documenting changes in typeclasses | 2016-10-29 | |
| | |_|_|/ / | |/| | | | | |||
| * | | | | | Merge remote-tracking branch 'github/pr/321' into v8.6 | 2016-10-28 | |
| |\ \ \ \ \ | |||
| * | | | | | | Using msg_info for info_auto and info_eauto (PR #324). | 2016-10-26 | |
| * | | | | | | Merge branch 'v8.5' into v8.6 | 2016-10-26 | |
| |\ \ \ \ \ \ | |||
| | * \ \ \ \ \ | Merge remote-tracking branch 'github/pr/338' into v8.5 | 2016-10-25 | |
| | |\ \ \ \ \ \ | |||
| | | * | | | | | | Remove warning now that info_auto is fixed. | 2016-10-25 | |
| | | | | * | | | | Remove v62 from the codebase. | 2016-10-25 | |
| | |_|_|/ / / / | |/| | | | | | | |||
| | * | | | | | | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | 2016-10-25 | |
| | |/ / / / / | |||
| | | | * / / | Fix printing of typeclasses eauto debug wrt intro. | 2016-10-24 | |
| | |_|/ / / | |/| | | | | |||
| | * | | | | Fixing printing of generic arguments of tag "var". | 2016-10-22 | |
| | | | * | | Renamings to avoid confusion deprecating old names | 2016-10-22 | |
| | |_|/ / | |/| | | | |||
| | | * | | sections/hints: prevent Not_found in get_type_of | 2016-10-21 | |
| | |/ / | |/| | | |||
* | | | | Merge branch 'v8.6' | 2016-10-17 | |
|\| | | | |||
| * | | | Merge branch 'v8.5' into v8.6 | 2016-10-17 | |
| |\| | | |||
| | * | | Still a problem with debug auto printing. | 2016-10-15 |