Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-23 |
|\ | |||
| * | Merge PR#480: show unused intro pattern warning | Maxime Dénès | 2017-03-22 |
| |\ | |||
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-03-22 |
|\| | | |||
* | | | Attempt to improve error message when "apply in" fail. | Hugo Herbelin | 2017-03-15 |
| | * | Show unused-intro-pattern warning. | Théo Zimmermann | 2017-03-14 |
| * | | Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals correc... | Maxime Dénès | 2017-03-10 |
| |\ \ | | |/ | |/| | |||
* | | | Proofview: tclINDEPENDENTL | Enrico Tassi | 2017-02-10 |
* | | | Fixing injection in the presence of let-in in constructors. | Hugo Herbelin | 2016-12-22 |
* | | | Merge remote-tracking branch 'github/pr/172' into trunk | Maxime Dénès | 2016-12-19 |
|\ \ \ | |||
* \ \ \ | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-12-07 |
|\ \ \ \ | | |/ / | |/| | | |||
| * | | | Merge remote-tracking branch 'github/pr/381' into v8.6 | Maxime Dénès | 2016-12-02 |
| |\ \ \ | |||
| | * | | | Fix shelving order in typeclasses eauto. | Théo Zimmermann | 2016-11-30 |
| | * | | | Fix typeclasses eauto shelving. | Théo Zimmermann | 2016-11-30 |
| * | | | | Fix bug #5232: proper globalization of hints paths | Matthieu Sozeau | 2016-11-30 |
| |/ / / | |||
* | | | | Tests for info/debug auto/eauto. | Hugo Herbelin | 2016-11-19 |
* | | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2016-11-18 |
|\| | | | |||
| * | | | Minor debug printing bug, | Matthieu Sozeau | 2016-11-16 |
| * | | | Revert more of a477dc for good measure | Matthieu Sozeau | 2016-11-16 |
| * | | | 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 |
| |\ \ \ | |||
| | * | | | Fixes to compile with ocaml 4.01 | Matthieu Sozeau | 2016-11-07 |
| * | | | | Merge commit 'e6edb33' into v8.6 | Maxime Dénès | 2016-11-07 |
| |\ \ \ \ | |||
| | * | | | | More explicit name for status of unification constraints. | Maxime Dénès | 2016-11-07 |
| * | | | | | More precise refine compatibility | Matthieu Sozeau | 2016-11-05 |
| * | | | | | Fix #3441 Use pf_get_type_of to avoid blowup | Matthieu Sozeau | 2016-11-04 |
| * | | | | | Fix refine in compatibility mode | Matthieu Sozeau | 2016-11-04 |
| * | | | | | Merge remote-tracking branch 'github/pr/335' into v8.6 | Maxime Dénès | 2016-11-04 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge remote-tracking branch 'github/pr/336' 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 |
|\| | | | | | | | |||
| | | | | * | | | Documenting changes in typeclasses | Matthieu Sozeau | 2016-10-29 |
| | |_|_|/ / / | |/| | | | | | |||
| * | | | | | | Merge remote-tracking branch 'github/pr/321' into v8.6 | Maxime Dénès | 2016-10-28 |
| |\ \ \ \ \ \ | |||
| * | | | | | | | Using msg_info for info_auto and info_eauto (PR #324). | Hugo Herbelin | 2016-10-26 |
| * | | | | | | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2016-10-26 |
| |\ \ \ \ \ \ \ | |||
| | * \ \ \ \ \ \ | Merge remote-tracking branch 'github/pr/338' into v8.5 | Maxime Dénès | 2016-10-25 |
| | |\ \ \ \ \ \ \ | |||
| | | * | | | | | | | Remove warning now that info_auto is fixed. | Théo Zimmermann | 2016-10-25 |
| | | | | * | | | | | Remove v62 from the codebase. | Théo Zimmermann | 2016-10-25 |
| | |_|_|/ / / / / | |/| | | | | | | | |||
| | * | | | | | | | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | Maxime Dénès | 2016-10-25 |
| | |/ / / / / / | |||
| | | | * / / / | Fix printing of typeclasses eauto debug wrt intro. | Théo Zimmermann | 2016-10-24 |
| | |_|/ / / / | |/| | | | | | |||
| | * | | | | | Fixing printing of generic arguments of tag "var". | Hugo Herbelin | 2016-10-22 |