| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-03-26 | Never store persistent arrays as VM structured values. | Pierre-Marie Pédrot | |
| Bytecode execution of persistent arrays can modify structured values meant to be marshalled in vo files. Some VM values are not marshallable, leading to this anomaly. There are further issues with the use of a hash table to store structured values, since they rely on structural equality and hashing functions. Persistent arrays are not safe in this context. Fixes #14006: Coqc cannot save .vo files containing primitive arrays. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |