coq/dev/doc/critical-bugs, branch master The formal proof system Document as critical. 2021-03-26T14:18:28+00:00 Guillaume Melquiond 2021-03-25T14:03:03+00:00 7ff8b12c14867e43d54c3d4c8976a6179250893d 






Add an entry to file critical-bugs.
2021-02-17T08:53:26+00:00

Guillaume Melquiond

2021-02-17T08:53:26+00:00

c150f3ab8dc9d1824d88b6fb9b1da14cb544ffc7












Make sure accumulators do not exceed the minor heap (partly fix #11170).
2020-11-20T16:59:18+00:00

Guillaume Melquiond

2020-11-20T16:59:18+00:00

2535afa1b1b5c74b4620d607dc46f3ef6e88d548

Accumulators can grow arbitrarily large, even when well-typed. So, this
commit makes sure they are allocated on the major heap when they are too
large. If so, fields need to be filled with caml_initialize, in case they
point to the minor heap.





Accumulators can grow arbitrarily large, even when well-typed. So, this
commit makes sure they are allocated on the major heap when they are too
large. If so, fields need to be filled with caml_initialize, in case they
point to the minor heap.







Add documentation about the soundness bug.
2020-11-12T09:58:46+00:00

Pierre-Marie Pédrot

2020-11-10T12:20:15+00:00

aa6d64c7de5d75f1a2625a3ec99c3efc699c5440












Update dev/doc/critical-bugs
2020-06-09T13:05:55+00:00

Pierre Roux

2020-06-09T09:36:41+00:00

9c76e6b4c9ae24826668fa9f72faf93e5d4c6acf












Fix #11421 computation of Set+2
2020-01-22T13:50:15+00:00

Gaëtan Gilbert

2020-01-18T13:46:05+00:00

71aa415282a93a6e23af3b824f8531c58d2d66bd












Add critical-bugs entry, tests-suite file, and code comment.
2019-12-27T14:53:38+00:00

Guillaume Melquiond

2019-12-27T05:04:39+00:00

00c0b652311b8c6b26c7e21b17db4ab12a35f286












Fix #11039: proof of False with template poly and nonlinear universes
2019-11-26T10:28:55+00:00

Gaëtan Gilbert

2019-11-15T14:53:48+00:00

a5d124dd7c3d43a5ead81cfac30c7d1448002d56

Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.

A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.

Also fixes #10504.





Using the parameter universes in the constructor causes implicit
equality constraints, so those universes may not be template
polymorphic.

A couple types in the stdlib were erroneously marked template, which
is now detected. Removing the marking doesn't actually change
behaviour though.

Also fixes #10504.







The "univ poly can capture global univs" checker side bug is fixed
2019-11-07T14:05:51+00:00

Gaëtan Gilbert

2019-11-04T15:28:09+00:00

7233d98a79894c6be1cbe99d003982b0f6a5c37b

(by the checker refactor AFAICT)

+ fix commit for the coqtop side fix (it got rebased at some point)

Close #10705





(by the checker refactor AFAICT)

+ fix commit for the coqtop side fix (it got rebased at some point)

Close #10705







Fix a De Bruijn bug in the computation of term relevance in the kernel.
2019-10-16T08:57:47+00:00

Pierre-Marie Pédrot

2019-10-15T19:33:31+00:00

5c5790d587ad425a882ea8bcdcf28d5ac046aaa3

Opening up a lambda should always lift the substitution attached to it.





Opening up a lambda should always lift the substitution attached to it.