Bool: iff lemmas about or, a reflect inductive, an is_true function

 For the moment, almost no lemmas about (reflect P b), just the proofs
 that it is equivalent with an P<->b=true.

 is_true b is (b=true), and is meant to be added as a coercion
 if one wants it. In the StdLib, this coercion is not globally
 activated, but particular files are free to use Local Coercion...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13275 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions