9ba52e1735
- Update to version 8.14.1.
* Fixed the implementation of persistent arrays used by the VM
and native compute so that it uses a uniform representation.
Previously, storing primitive floats inside primitive arrays
could cause memory corruption.
* Fixed missing registration of universe constraints in Module
Type elaboration.
* Made `abstract` more robust with respect to Ltac `constr`
bindings containing existential variables.
* Correct support of trailing `let` by tactic `specialize`.
* Fixed an anomaly with `Extraction Conservative Types` when
extracting pattern-matching on singleton types.
* Regular error instead of an anomaly when calling `Separate
Extraction` in a module.
OBS-URL: https://build.opensuse.org/request/show/940115
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/coq?expand=0&rev=14
|
||
|---|---|---|
| _constraints | ||
| .gitattributes | ||
| .gitignore | ||
| coq-8.14.1.tar.gz | ||
| coq-refman-8.14.1.tar.xz | ||
| coq-rpmlintrc | ||
| coq-stdlib-8.14.1.tar.xz | ||
| coq.changes | ||
| coq.desktop | ||
| coq.spec | ||
| coq.xml | ||