From 25fcadf68ae22e56dbe7ab27060bd28cdc63a9af Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 1 Feb 2024 14:46:53 +0100 Subject: [PATCH] Remove lot of Canonical in favor of Export (canonical) --- classical/contra.v | 71 +--------------------------------------------- 1 file changed, 1 insertion(+), 70 deletions(-) diff --git a/classical/contra.v b/classical/contra.v index 6f158e4829..e192fe8c1e 100644 --- a/classical/contra.v +++ b/classical/contra.v @@ -746,76 +746,7 @@ Proof. by rewrite 2!lax_notE. Qed. End Internals. Import 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. +Export (canonicals) Internals. (******************************************************************************) (* Lemma and tactic assume_not: add a goal negation assumption. The tactic *)