Coq para Mac

• Cambiado: Teoremas mutuamente probados con declaraciones en diferentes tipos coinductivos ahora soportados (#18743, por Hugo Herbelin).
• Añadido: CoFixpoint soporta atributos bypass_guard, clearbody, deprecated y warn (#18754, por Hugo Herbelin).
• Añadido: Program Fixpoint con medida o wf (ver Program Fixpoint) ahora soporta la cláusula where para notaciones, los atributos local y clearbody, así como conclusiones no atómicas (#18834, por Hugo Herbelin, arreglos en particular #13812 y #14841).
• Corregido: Anomalía en la ausencia de obligaciones restantes de algunos nombres ahora es un error (#18873, arregla #3889, por Hugo Herbelin).
• Corregido: Las obligaciones del Programa polimórfico de universo ahora se generalizan solo sobre las variables de universo que efectivamente ocurren en la obligación (#18915, arregla #11766 y #11988, por Hugo Herbelin).
• Corregido: Fallo de aserción de anomalía en la compilación de coincidencias de patrones, con Modo Programa o con let-ins en la aridad de un tipo inductivo (#18921, arregla #5777 y #11030 y #11586, por Hugo Herbelin).
• Corregido: Soporte para coincidencias de patrones al estilo Programa en más de un argumento en una familia inductiva (#18929, arregla #1956 y #5777, por Hugo Herbelin).
• Corregido: anomalía con obligaciones en los enlaces de un Programa Fixpoint basado en medida o wf (#18958, arregla #18920, por Hugo Herbelin).
• Corregido: Registro incorrecto de nombres de universo adjuntos a una constante polimórfica primitiva (#19100, arregla #19099, por Hugo Herbelin).

Lista completa de cambios disponible aquí