Skip to content

Commit

Permalink
Remove lot of Canonical in favor of Export (canonical)
Browse files Browse the repository at this point in the history
  • Loading branch information
proux01 committed Feb 9, 2024
1 parent b514818 commit 9e6faf9
Showing 1 changed file with 1 addition and 70 deletions.
71 changes: 1 addition & 70 deletions classical/contra.v
Original file line number Diff line number Diff line change
Expand Up @@ -747,76 +747,7 @@ Proof. by rewrite 2!lax_notE. Qed.
End Internals.
Import Internals.
Hint View for move/ move_viewP|2.
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 *)
Expand Down

0 comments on commit 9e6faf9

Please sign in to comment.