aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
Was PR#339: Documenting type class options, typeclasses eauto
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
They allow to call refine without doing typeclass resolution, allowing to use refine in typeclass hints.
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
Was PR#331: Solve_constraints and Set Use Unification Heuristics
2016-11-07Improve formatting of a message in [Arguments].Maxime Dénès
2016-11-07Fix #5181: [Arguments] no longer correctly checks the length of arguments listsMaxime Dénès
2016-11-07Fix #5182: "Arguments names must be distinct." is bogus and underinformativeMaxime Dénès
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-11-05Not using style tags when translating/beautifying a file.Hugo Herbelin
2016-11-05Removing a special treatment for empty lines in comments.Hugo Herbelin
This made the whole pp code complicated only for the purpose of the beautifier, while it is not clear when this was useful. Removing the code for simplicity, not excluding to later address beautifier issues when they show up.
2016-11-05Removing obsolete parsing of strings à la v7 in comments.Hugo Herbelin
This was for the translator and is not relevant for the beautifier.
2016-11-05Do not print dependent evars by default (expensive)Matthieu Sozeau
The option can be turned on by the user though.
2016-11-05More precise refine compatibilityMatthieu Sozeau
2016-11-04Quick fix of tactic parsing while Load-ing in coqide.Hugo Herbelin
Note that this is still broken when loading files containing C-zar scripts.
2016-11-04Test for #4966 ("auto" wrongly seen as "auto with *" when in position of ident).Hugo Herbelin
2016-11-04Fix #3441 Use pf_get_type_of to avoid blowupMatthieu Sozeau
... in pose proof of large proof terms
2016-11-04Fix refine in compatibility modeMatthieu Sozeau
2016-11-04Fix #4837: ./configure -local makes coqdep issue many warningsMaxime Dénès
We simply remove the warnings about paths mixing Win32 and Unix separators, since that situation does not seem problematic (c.f. discussion on the bug tracker).
2016-11-04Merge remote-tracking branch 'github/pr/335' into v8.6Maxime Dénès
Was PR#335: Fix printing of typeclasses eauto debug wrt intro.
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
Was PR#336: Remove v62
2016-11-04Add documentation for [Set Warnings] and the -w option.Cyprien Mangin
2016-11-04Silence option deprecation warnings in the compat fileJason Gross
Some options are expected to be deprecated
2016-11-03Remove an OCaml 4.02 construct.Maxime Dénès
This was not detected by running coq-contribs, so it probably means that we are not testing with the right version of OCaml.
2016-11-03Merge remote-tracking branch 'github/pr/340' into v8.6Maxime Dénès
Was PR#340: Fix various shortcomings of the warnings infrastructure.
2016-11-03Rework search_strategy option handlingMatthieu Sozeau
2016-11-03Internal API change to typeclasses eauto.Théo Zimmermann
This commit makes the traversing strategy of typeclasses eauto an optional argument of the function that implements it. This change should be non-breaking.
2016-11-03Do not shelve non-class subgoals but fail, it shouldMatthieu Sozeau
be the instance writer's responsibility to not generated non-dependent non-class subgoals (otherwise we loose compatibility as shown in e.g. MathClasses, which goes into loops because of unexpectedly unconstrained goals). Reflect it in the doc.
2016-11-03Fix test-suite files relying on tcs bugsMatthieu Sozeau
- One was expecting shelved goals to remain after resolution (from refine). - The other too were relying on the wrong classification of subgoals as typeclass subgoals at toplevel.
2016-11-03Fixed bug #4095.Matthieu Sozeau
2016-11-03typeclasses eauto Implem/doc of shelving strategyMatthieu Sozeau
Now [typeclasses eauto] mimicks what happens during resolution faithfully, and the shelving behavior/requirements for a successful proof-search are documented.
2016-11-03Fix [typeclasses eauto with] and nopattern hintsMatthieu Sozeau
This was the source of a bug in #5115#c7.
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
In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
2016-11-03Document options of typeclasses (eauto)Matthieu Sozeau
With update after J. Gross comments
2016-11-03Merge remote-tracking branch 'github/pr/341' into v8.6Maxime Dénès
Was PR#341: Better Arguments compatibility.
2016-11-02Better Arguments compatibility.Maxime Dénès
With multiple arguments list, repeating the "/" modifier used to be mandatory. So instead of forbidding it, we issue a deprecation warning.
2016-11-02Fix various shortcomings of the warnings infrastructure.Maxime Dénès
- The flags are now interpreted from left to right, without any other precedence rule. The previous one did not make much sense in interactive mode. - Set Warnings and Set Warnings Append are now synonyms, and have the "append" semantics, which is the most natural one for warnings. - Warnings on unknown warnings are now printed only once (previously the would be repeated on further calls to Set Warnings, sections closing, module requiring...). - Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced to "-foo" (if foo exists, "" otherwise).
2016-11-02Put string between quotes when printing an option value.Maxime Dénès
This is a better (more generic) fix to #5061 than my e8b9ee76.
2016-10-30Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-29Removing dead code.Hugo Herbelin
2016-10-29Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).Hugo Herbelin
(May it fell in the case mentioned in the inner comment of Exninfo.info?)
2016-10-29Documenting changes in typeclassesMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 17:55:32 +0000