Zorn etc. (Co-Authored by Georges Gonthier <[email protected]>)

_CoqProject

@@ -11,6 +11,7 @@
 classical/all_classical.v
 classical/boolp.v
 classical/contra.v
+classical/wochoice.v
 classical/classical_sets.v
 classical/mathcomp_extra.v
 classical/functions.v

classical/Make

@@ -9,6 +9,7 @@
 
 boolp.v
 contra.v
+wochoice.v
 classical_sets.v
 mathcomp_extra.v
 functions.v

classical/contra.v

@@ -779,6 +779,76 @@ Hint View for move/ move_viewP|2.
 Hint View for move/ Internals.equivT_LR|2 Internals.equivT_RL|2.
 Hint View for apply/ Internals.equivT_RL|2 Internals.equivT_LR|2.
 Export (canonicals) Internals.
+Canonical TypeForall.
+Canonical PropForall.
+Canonical SetForall.
+Canonical wrap1Prop.
+Canonical wrap1Type.
+Canonical proper_nProp.
+Canonical trivial_nProp.
+Canonical True_nProp.
+Canonical False_nProp.
+Canonical not_nProp.
+Canonical and_nProp.
+Canonical and3_nProp.
+Canonical and4_nProp.
+Canonical and5_nProp.
+Canonical or_nProp.
+Canonical or3_nProp.
+Canonical or4_nProp.
+Canonical unary_and_rhs.
+Canonical binary_and_rhs.
+Canonical imply_nProp.
+Canonical exists_nProp.
+Canonical exists2_nProp.
+Canonical inhabited_nProp.
+Canonical forall_nProp.
+Canonical proper_nBody.
+Canonical nonproper_nBody.
+Canonical bounded_nBody.
+Canonical unbounded_nBody.
+Canonical is_true_nProp.
+Canonical true_neg.
+Canonical true_pos.
+Canonical false_neg.
+Canonical false_pos.
+Canonical id_neg.
+Canonical id_pos.
+Canonical negb_neg.
+Canonical negb_pos.
+Canonical neg_ltn_LHS.
+Canonical neg_leq_LHS.
+Canonical leq_neg.
+Canonical eq_nProp.
+Canonical bool_neq.
+Canonical true_neq.
+Canonical false_neq.
+Canonical eqType_neq.
+Canonical eq_op_pos.
+Canonical Prop_wType.
+Canonical proper_wType.
+Canonical forall_wType.
+Canonical inhabited_wType.
+Canonical void_wType.
+Canonical unit_wType.
+Canonical pair_wType.
+Canonical sum_wType.
+Canonical sumbool_wType.
+Canonical sumor_wType.
+Canonical sig1_wType.
+Canonical sig2_wType.
+Canonical sigT_wType.
+Canonical sigT2_wType.
+Canonical proper_wProp.
+Canonical forall_wProp.
+Canonical trivial_wProp.
+Canonical inhabited_wProp.
+Canonical nand_false_bool.
+Canonical nand_true_bool.
+Canonical and_wProp.
+Canonical or_wProp.
+Canonical exists_wProp.
+Canonical exists2_wProp.
 
 (******************************************************************************)
 (* Lemma and tactic assume_not: add a goal negation assumption. The tactic    *)