Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove lot of Canonical in favor of Export (canonical) #1172

Merged
merged 2 commits into from
Feb 9, 2024
Merged

Remove lot of Canonical in favor of Export (canonical) #1172

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b514818
Missing reexport of Hint
proux01 Feb 9, 2024
9e6faf9
Remove lot of Canonical in favor of Export (canonical)
proux01 Feb 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
72 changes: 2 additions & 70 deletions classical/contra.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -746,76 +746,8 @@ 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.
Hint View for move/ move_viewP|2.
Export (canonicals) Internals.

(******************************************************************************)
(* Lemma and tactic assume_not: add a goal negation assumption. The tactic *)
Expand Down
Loading