HoTT/HoTT — pull request #528 by marcbezem (2014-09-26 20:16:19+00:00)
Title: Fixed False_hp, added Negation_hp

Question: where to place (in HProp.v, Bool.v, Misc.v, HoTTBookExercises.v, or elsewhere)?
Require Import Bool.
(** canonical map from Bool to hProp *)
Definition Bool_to_hProp (b : Bool) : hProp
:= if b then Unit_hp else False_hp.

In HProp.v this gave an unexpected error ("Bool not found in the current environment") with the latest coq-scripts @ a87e3ca, while it had been typechecked correctly before.