aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-12-05the -byte option is deprecatedPaul Steckler
2016-12-05Compute dependency of C files only in kernel/byterun.Maxime Dénès
Some C files included in build scripts (in dev/build) were triggering errors or warnings on non-win32 platforms. Note that ide/ide_win32_stubs.c was already handled through an ad-hoc rule in Makefile. If you add a new C file outside of kernel/byterun, please extend the CFILES variable.
2016-12-04Merge remote-tracking branch 'github/pr/366' into v8.6Maxime Dénès
Was PR#366: Univs: fix bug 5208
2016-12-04Merge remote-tracking branch 'github/pr/378' into v8.6Maxime Dénès
Was PR#378: Univs: fix bug #5188
2016-12-02Fix test-suite after change in "context" printing.Maxime Dénès
2016-12-02Document changesMatthieu Sozeau
2016-12-02Merge remote-tracking branch 'github/pr/377' into v8.6Maxime Dénès
Was PR#377: Univs: fix bug #5180
2016-12-02Merge remote-tracking branch 'github/pr/372' into v8.6Maxime Dénès
Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes
2016-12-02Merge remote-tracking branch 'github/pr/368' into v8.6Maxime Dénès
Was PR#368: Add example in dev/doc/changes involving Tacmach.project
2016-12-02Merge branch 'pr/367' into v8.6Maxime Dénès
Parts of PR#367: Fixing the "beautifier" and checking the parsing-printing reversibility
2016-12-02Fixing lexing of strings in comments for beautifier.Hugo Herbelin
Was a bug introduced in 0ad6edc1.
2016-12-02Fixing printing of "ltac:" in tactics after surrounding parenthesesHugo Herbelin
became mandatory.
2016-12-02Comment on universe handling in ParametersMatthieu Sozeau
2016-12-02Univs: fix bug #5188Matthieu Sozeau
Parameter was implemented the wrong way trying to separate the universes of the telescope.
2016-12-02Merge remote-tracking branch 'github/pr/381' into v8.6Maxime Dénès
Was PR#381: V8.6+fix typeclasses eauto shelving
2016-12-02Fix #5242 - Dubious unsilenceable warning on invalid identifierMaxime Dénès
We make this warning configurable and disabled by default.
2016-12-02Fixing printing of "Set Warnings Append".Hugo Herbelin
2016-12-02Fixing space in printing "Context".Hugo Herbelin
2016-12-02Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-12-02Fixing space in printing several list of implicit arguments.Hugo Herbelin
2016-12-02Fixing printing of "only parsing" in abbreviations.Hugo Herbelin
2016-12-02Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
with user-level notations by inserting spaces.
2016-12-02More on fixing #5098 (preserving printing of "in hyp").Hugo Herbelin
2016-12-02Merge remote-tracking branch 'github/pr/380' into v8.6Maxime Dénès
Was PR#380: Fix bug #5232: proper globalization of hints paths
2016-12-02Merge remote-tracking branch 'github/pr/369' into v8.6Maxime Dénès
Was PR#369: Make a note about wit_constr and Constrarg in dev/doc/changes
2016-12-02Merge remote-tracking branch 'github/pr/371' into v8.6Maxime Dénès
Was PR#371: Update dev/doc/changes with things about mem_named_context
2016-12-02Merge remote-tracking branch 'github/pr/364' into v8.6Maxime Dénès
Was PR#364: Add missing label. Fixes broken ref.
2016-12-02Merge remote-tracking branch 'github/pr/382' into v8.6Maxime Dénès
Was PR#382: [merlin] Adjust merlin for ide.
2016-11-30[merlin] Adjust merlin for ide.Emilio Jesus Gallego Arias
2016-11-30Fix shelving order in typeclasses eauto.Théo Zimmermann
Before this fix, unshelve typeclasses eauto would produce sub-goals in the reverse order compared to when they were first shelved.
2016-11-30Fix typeclasses eauto shelving.Théo Zimmermann
A file in the test-suite had to be modified. It was supposed to reproduce a behavior in intuistionistic-nuprl but it did not really. This commit is not supposed to break intuistionistic-nuprl.
2016-11-30Fix bug #5232: proper globalization of hints pathsMatthieu Sozeau
2016-11-30Univs: fix bug #5180Matthieu Sozeau
In the kernel's generic conversion, backtrack on UniverseInconsistency for the unfolding heuristic (single backtracking point in reduction). This exception can be raised in the univ_compare structure to produce better error messages when the generic conversion function is called from higher level code in reductionops.ml, which itself is called during unification in evarconv.ml. Inside the kernel, the infer and check variants of conversion never raise UniverseInconsistency though, so this does not change the behavior of the kernel.
2016-11-30Fix UGraph.check_eq!Matthieu Sozeau
Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code
2016-11-30Slightly more efficient [Univ.super] implemMatthieu Sozeau
2016-11-30Fix #5183 - Two CoqIDE crash errorsMaxime Dénès
When opening a file without extension, an uncaught exception was occurring. Note that this fix is not complete, since the "Compile Buffer" command still fails. This is because of a limitation of coqc which appends the ".v" extension to its argument even if it already existed (and even if it doesn't exist with the extension!).
2016-11-30Update copyright on documentation cover.Maxime Dénès
2016-11-30Fix #5174: Underinformative syntax error messages in the new arguments syntaxMaxime Dénès
We introduce a bit of compatibility parsing code to print deprecation warnings.
2016-11-29STM: cur_id must be invalid if an error occurs (fix #5191)Enrico Tassi
Line erroneously removed in 17f3346c
2016-11-24Fix some documentation typos.Guillaume Melquiond
Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
2016-11-24Lazily load constants in micromega (bug #5134).Guillaume Melquiond
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-24Fix incorrect long multiplication in the VM.Guillaume Melquiond
If the result had its 30th bit set, then all the high part of the result on a 64-bit architecture would end up being set, thus breaking subsequent computations. This patch also fixes the incorrectly parenthesized definition of uint32_of_value, which by luck was never misused.
2016-11-22Properly parenthesize "ltac:" arguments (bug #5169).Guillaume Melquiond
2016-11-21(v8.6) Update dev/doc/changes.txt with HintsResolveEntry changesJason Gross
2016-11-21(v8.6) Update dev/doc/changes with things about mem_named_contextJason Gross
2016-11-21(v8.6) Make a note about wit_constr and Constrarg in dev/doc/changesJason Gross
2016-11-21(v8.6) Add example in dev/doc/changes involving Tacmach.projectJason Gross
2016-11-21Remove spurious spaces in merlin file generated by coq_makefile (bug #5213).Guillaume Melquiond
2016-11-21Stop parsing -compat-notations options, which are no longer supported (bug ↵Guillaume Melquiond
#3339).
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 21:43:13 +0000