Coq for Mac

• Changed: Mutually-proved theorems with statements in different coinductive types now supported (#18743, by Hugo Herbelin).
• Added: CoFixpoint supports attributes bypass_guard, clearbody, deprecated and warn (#18754, by Hugo Herbelin).
• Added: Program Fixpoint with measure or wf (see Program Fixpoint) now supports the where clause for notations, the local and clearbody attributes, as well as non-atomic conclusions (#18834, by Hugo Herbelin, fixes in particular #13812 and #14841).
• Fixed: Anomaly on the absence of remaining obligations of some name now an error (#18873, fixes #3889, by Hugo Herbelin).
• Fixed: Universe polymorphic Program's obligations are now generalized only over the universe variables that effectively occur in the obligation (#18915, fixes #11766 and #11988, by Hugo Herbelin).
• Fixed: Anomaly assertion failed in pattern-matching compilation, with Program Mode or with let-ins in the arity of an inductive type (#18921, fixes #5777 and #11030 and #11586, by Hugo Herbelin).
• Fixed: Support for Program-style pattern-matching on more than one argument in an inductive family (#18929, fixes #1956 and #5777, by Hugo Herbelin).
• Fixed: anomaly with obligations in the binders of a measure- or wf-based Program Fixpoint (#18958, fixes #18920, by Hugo Herbelin).
• Fixed: Incorrect registration of universe names attached to a primitive polymorphic constant (#19100, fixes #19099, by Hugo Herbelin).

Full list of changes available here