Leonardo de Moura 8295ef4e57 fix(library/tactic/class_instance_synth): constraint execution order at type class resolution ... We could not fix this problem before because we did not have the [quasireducible] annotation. Without this annotation, the fixed TC would loop in some HoTT files.		2015-03-04 22:20:20 -08:00
..
algebra	fix(library/tactic/class_instance_synth): constraint execution order at type class resolution	2015-03-04 22:20:20 -08:00
init	fix(library/tactic/class_instance_synth): constraint execution order at type class resolution	2015-03-04 22:20:20 -08:00
types	feat(*.md): create markdown files for HoTT library, update ones in standard library	2015-03-04 18:33:18 -08:00
.project	feat(*): add support for separate HoTT library	2014-12-05 14:34:02 -08:00
hott.md	feat(*.md): create markdown files for HoTT library, update ones in standard library	2015-03-04 18:33:18 -08:00