aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-11-07Mention notypeclasses refine in CHANGESMatthieu Sozeau
2016-11-07CHANGES for this branch.Matthieu Sozeau
2016-11-07Document two new variants of refineMatthieu Sozeau
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
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-03Fix test-suite files relying on tcs bugsMatthieu Sozeau
2016-11-03Fixed bug #4095.Matthieu 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-03Test new syntax for hints and typeclass optionsMatthieu 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-11-03Document options of typeclasses (eauto)Matthieu Sozeau
2016-10-29Documenting changes in typeclassesMatthieu Sozeau
2016-10-29Fixing #5164 (regression in locating error in argument of "refine").Hugo Herbelin
2016-10-28Merge remote-tracking branch 'github/pr/321' into v8.6Maxime Dénès
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
2016-10-28Merge commit 'fccbd64' into v8.6Maxime Dénès
2016-10-28[build] Add a target to install the META file.Emilio Jesus Gallego Arias
2016-10-28[build] META file to enable plugin linking with ocamlfind.Emilio Jesus Gallego Arias
2016-10-28Merge remote-tracking branch 'github/pr/337' into v8.6Maxime Dénès
2016-10-27Add missing dot to impargs error message.Maxime Dénès
2016-10-27Proper fix for #3753 (anomaly with implicit arguments and renamings)Maxime Dénès
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-26Using msg_info for info_auto and info_eauto (PR #324).Hugo Herbelin
2016-10-26STM: make ~valid state id non optional from APIsEnrico Tassi
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-25Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Maxime Dénès
2016-10-25Merge commit 'a799600' into v8.6Maxime Dénès
2016-10-25That Function is unable to create a Fixpoint equation is a user problem,Yves Bertot
2016-10-25Update CHANGES.Maxime Dénès
2016-10-25Bump version number to 8.5pl3.Maxime Dénès
2016-10-25Merge remote-tracking branch 'github/pr/333' into v8.5Maxime Dénès
2016-10-25Merge remote-tracking branch 'github/pr/329' into v8.5Maxime Dénès
2016-10-24Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-24Adding a test for #4398 (interpretation scopes for "match goal").Hugo Herbelin
2016-10-24Rename lia.cache into .lia.cache in the test-suite Makefile.Maxime Dénès
2016-10-24Merge commit '81bdc22' into v8.6Maxime Dénès
2016-10-24Merge remote-tracking branch 'github/pr/326' into v8.5Maxime Dénès
2016-10-24Test file for #5127: Memory corruption with the VMMaxime Dénès
2016-10-24Fix #5127 Memory corruption with the VMMaxime Dénès
2016-10-24Merge branch 'v8.5' into v8.6Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 13:14:03 +0000