Coq pour Mac

• Modifié : Les théorèmes prouvés mutuellement avec des énoncés dans différents types coinductifs sont maintenant pris en charge (#18743, par Hugo Herbelin).
• Ajouté : CoFixpoint prend en charge les attributs bypass_guard, clearbody, deprecated et warn (#18754, par Hugo Herbelin).
• Ajouté : Program Fixpoint avec mesure ou wf (voir Program Fixpoint) prend maintenant en charge la clause where pour les notations, les attributs local et clearbody, ainsi que des conclusions non atomiques (#18834, par Hugo Herbelin, corrige en particulier #13812 et #14841).
• Corrigé : Anomalie sur l'absence d'obligations restantes de certains noms maintenant une erreur (#18873, corrige #3889, par Hugo Herbelin).
• Corrigé : Les obligations polymorphiques de l'univers du Programme sont maintenant généralisées uniquement sur les variables d'univers qui apparaissent effectivement dans l'obligation (#18915, corrige #11766 et #11988, par Hugo Herbelin).
• Corrigé : Échec d'assertion d'anomalie dans la compilation de correspondance de motifs, avec le Mode Programme ou avec des let-ins dans l'arity d'un type inductif (#18921, corrige #5777 et #11030 et #11586, par Hugo Herbelin).
• Corrigé : Support pour la correspondance de motifs de style Programme sur plus d'un argument dans une famille inductive (#18929, corrige #1956 et #5777, par Hugo Herbelin).
• Corrigé : anomalie avec les obligations dans les liaisons d'un Programme basé sur une mesure ou wf (#18958, corrige #18920, par Hugo Herbelin).
• Corrigé : Enregistrement incorrect des noms d'univers attachés à une constante polymorphique primitive (#19100, corrige #19099, par Hugo Herbelin).

Liste complète des changements disponible ici