aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-11-08Complete a truncated commentArnaud Spiwack
Introduce by myself, I'm afraid, in #308. Noticed by PMP during the review, but I forgot to fix it before merge.
2016-11-08tclDISPATCH: more informative error messageArnaud Spiwack
"expected _n_ tactics" -> "exected _n_ tactics, was given _k_". Also affect other similar tacticals from `Proofview`. I used that for debugging once, I thought I might as well propose it for mergeing.
2016-11-07Ordering search: memoise relevance metricArnaud Spiwack
Recalculating the metric all the time was proving costly (it was obvious even on small queries).
2016-11-07Refine the relevance measureArnaud Spiwack
Having more disctinc symbols incurs a penalty.
2016-11-07Sort search results by relevanceArnaud Spiwack
This orders the results of search commands (such as `Search`, `SearchAbout`, …) according to a "relevance" metric to minimise. In this minimal version, the metric is the size of the displayed term.
2016-11-07After Emilio's comment.Matthieu Sozeau
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-07More accurate contributor list.Matthieu Sozeau
Command used: git log v8.5..HEAD --pretty=format:"%an," | sort -k 2 | uniq with some manual postprocessing for login names, particles and multiple first names.
2016-11-07Hugo and Maxime's 2nd pass of commentsMatthieu 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-06Hugo's commentsMatthieu Sozeau
2016-11-06Maxime's commentsMatthieu Sozeau
2016-11-06Fixes from Enrico's reviewMatthieu Sozeau
2016-11-05Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunkMatej Kosik
2016-11-05FIX: dev/includeMatej Kosik
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-05Credits for 8.6Matthieu Sozeau
2016-11-05Minor fix in documentationMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-16 05:41:47 +0000