Coq für Mac

• Änderung: Gegenseitig bewiesene Theoreme mit Aussagen in verschiedenen koinduktiven Typen jetzt unterstützt (#18743, von Hugo Herbelin).
• Hinzugefügt: CoFixpoint unterstützt Attribute bypass_guard, clearbody, deprecated und warn (#18754, von Hugo Herbelin).
• Hinzugefügt: Program Fixpoint mit Maß oder wf (siehe Program Fixpoint) unterstützt jetzt die where-Klausel für Notationen, die lokalen und clearbody-Attribute sowie nicht-atomare Schlussfolgerungen (#18834, von Hugo Herbelin, behebt insbesondere #13812 und #14841).
• Behoben: Anomalie bei der Abwesenheit verbleibender Verpflichtungen eines Namens jetzt ein Fehler (#18873, behebt #3889, von Hugo Herbelin).
• Behoben: Universum-polymorphe Verpflichtungen von Programmen sind jetzt nur über die Universumsvariablen verallgemeinert, die tatsächlich in der Verpflichtung auftreten (#18915, behebt #11766 und #11988, von Hugo Herbelin).
• Behoben: Anomalie bei fehlgeschlagener Assertion in der Musterabgleich-Kompilierung, mit Programm-Modus oder mit let-ins in der Arität eines induktiven Typs (#18921, behebt #5777 und #11030 und #11586, von Hugo Herbelin).
• Behoben: Unterstützung für Programmstil-Musterabgleich mit mehr als einem Argument in einer induktiven Familie (#18929, behebt #1956 und #5777, von Hugo Herbelin).
• Behoben: Anomalie mit Verpflichtungen in den Bindern eines Maß- oder wf-basierten Program Fixpoint (#18958, behebt #18920, von Hugo Herbelin).
• Behoben: Falsche Registrierung von Universumsnamen, die an eine primitive polymorphe Konstante angehängt sind (#19100, behebt #19099, von Hugo Herbelin).

Vollständige Liste der Änderungen verfügbar hier