HoTT/HoTT — pull request #27 by benediktahrens (2012-10-23 03:52:03+00:00)
Title: make constructions compile again

fixed two constructions which had not worked any more after some mods (which ones? triangle thingy? ssreflect? perhaps some rewrite working differently?)

Suggestion: restrict use of automation to *finish* a construction -- otherwise if automation behaviour changes, proof script breaks in the middle -> difficult to fix
This is particularly bad since we are following trunk and should expect frequent change in behaviour of Coq tactics.