HoTT/coq — pull request #60 by JasonGross (2013-09-26 17:49:32+00:00)
Title: Update the environment so discriminate works with eq in Type

The find_scheme function will modify the global environment to add an
induction scheme generated on the fly. We will fail if we look for the
generated induction scheme in the local environment, which hasn't been
updated.