aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-11-14Do not mention "none" in warnings doc, as it is there for compatibility.Maxime Dénès
2016-11-11Coqide: fixing default local links for refman and stdlib.Hugo Herbelin
2016-11-11Making explicit that a result is discarded (ocaml warning).Hugo Herbelin
2016-11-10Remove unused feedback_content: GoalsCJ Bell
2016-11-10Move OSX script.Maxime Dénès
2016-11-10Add Michael Soegtrop's new script to build windows installer.Maxime Dénès
2016-11-10Remove old windows build scripts.Maxime Dénès
2016-11-10Update CHANGES and credits for 8.6beta1.Maxime Dénès
2016-11-10Updating a comment in test-suite.Hugo Herbelin
2016-11-08Introducing a new EConstr.t type to perform the nf_evar operation on demand.Pierre-Marie Pédrot
2016-11-08Merge commit 'b385fbb' into v8.6Maxime Dénès
Was PR#347: Fix performance problem in pose proof
2016-11-08Use pf_get_type_of to avoid blowup in pose proof of large proof termsMatthieu Sozeau
2016-11-08Merge remote-tracking branch 'github/pr/348' into v8.6Maxime Dénès
Was PR#348: Credits for 8.6
2016-11-08Update documentation of Arguments after recent changes.Maxime Dénès
2016-11-08Rewording from EnricoMatthieu Sozeau
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).
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 20:04:14 +0000