aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2017-04-06Merge PR#508: Optimize pending evarsMaxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Fast path for implicit tactic solving.Pierre-Marie Pédrot
2017-03-23Ensuring static invariants about handling of pending evars in Pretyping.Pierre-Marie Pédrot
2017-03-22Merge PR#480: show unused intro pattern warningMaxime Dénès
2017-03-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-03-15Attempt to improve error message when "apply in" fail.Hugo Herbelin
2017-03-14Show unused-intro-pattern warning.Théo Zimmermann
2017-03-10Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals correc...Maxime Dénès
2017-02-10Proofview: tclINDEPENDENTLEnrico Tassi
2016-12-22Fixing injection in the presence of let-in in constructors.Hugo Herbelin
2016-12-19Merge remote-tracking branch 'github/pr/172' into trunkMaxime Dénès
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-02Merge remote-tracking branch 'github/pr/381' into v8.6Maxime Dénès
2016-11-30Fix shelving order in typeclasses eauto.Théo Zimmermann
2016-11-30Fix typeclasses eauto shelving.Théo Zimmermann
2016-11-30Fix bug #5232: proper globalization of hints pathsMatthieu Sozeau
2016-11-19Tests for info/debug auto/eauto.Hugo Herbelin
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-16Minor debug printing bug,Matthieu Sozeau
2016-11-16Revert more of a477dc for good measureMatthieu Sozeau
2016-11-15Revert part of a477dc, disallow_shelvedMatthieu Sozeau
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-11-05More precise refine compatibilityMatthieu Sozeau
2016-11-04Fix #3441 Use pf_get_type_of to avoid blowupMatthieu Sozeau
2016-11-04Fix refine in compatibility modeMatthieu Sozeau
2016-11-04Merge remote-tracking branch 'github/pr/335' into v8.6Maxime Dénès
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
2016-11-03Rework search_strategy option handlingMatthieu Sozeau
2016-11-03Internal API change to typeclasses eauto.Théo Zimmermann
2016-11-03Do not shelve non-class subgoals but fail, it shouldMatthieu Sozeau
2016-11-03typeclasses eauto Implem/doc of shelving strategyMatthieu Sozeau
2016-11-03Fix [typeclasses eauto with] and nopattern hintsMatthieu Sozeau
2016-11-03Fix handling of only_classes at toplevelMatthieu Sozeau
2016-11-03Handle Unique Solutions flag.Matthieu Sozeau
2016-11-03TCS: error handling and debug printing in resolutionMatthieu Sozeau
2016-11-03Fix bugs in Filtered Unification and cleanup codeMatthieu Sozeau
2016-11-03Fix Typeclasses eauto := bfs.Matthieu Sozeau
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-29Documenting changes in typeclassesMatthieu Sozeau
2016-10-28Merge remote-tracking branch 'github/pr/321' into v8.6Maxime Dénès
2016-10-26Using msg_info for info_auto and info_eauto (PR #324).Hugo Herbelin
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-25Merge remote-tracking branch 'github/pr/338' into v8.5Maxime Dénès
2016-10-25Remove warning now that info_auto is fixed.Théo Zimmermann
2016-10-25Remove v62 from the codebase.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 17:35:21 +0000