Changeset 985 for src/common

Timestamp:

Jun 16, 2011, 4:50:23 PM (10 years ago)

Author:

sacerdot

Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:

• src/common/AST.ma (modified) (1 diff)

src/common/AST.ma

@@ -599 +599 @@
 definition bool_to_Prop ≝
  λb. match b with [ true ⇒ True | false ⇒ False ].
+
+coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 
 
 (* dpm: should go to standard library *)