diff options
Diffstat (limited to 'theories/Relations/Operators_Properties.v')
| -rw-r--r-- | theories/Relations/Operators_Properties.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 21beac36f..f7f5512e7 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -17,17 +17,17 @@ Require Import Relation_Operators. Section Properties. - Implicit Arguments clos_refl_trans [A]. - Implicit Arguments clos_refl_trans_1n [A]. - Implicit Arguments clos_refl_trans_n1 [A]. - Implicit Arguments clos_refl_sym_trans [A]. - Implicit Arguments clos_refl_sym_trans_1n [A]. - Implicit Arguments clos_refl_sym_trans_n1 [A]. - Implicit Arguments clos_trans [A]. - Implicit Arguments clos_trans_1n [A]. - Implicit Arguments clos_trans_n1 [A]. - Implicit Arguments inclusion [A]. - Implicit Arguments preorder [A]. + Arguments clos_refl_trans [A] R x _. + Arguments clos_refl_trans_1n [A] R x _. + Arguments clos_refl_trans_n1 [A] R x _. + Arguments clos_refl_sym_trans [A] R _ _. + Arguments clos_refl_sym_trans_1n [A] R x _. + Arguments clos_refl_sym_trans_n1 [A] R x _. + Arguments clos_trans [A] R x _. + Arguments clos_trans_1n [A] R x _. + Arguments clos_trans_n1 [A] R x _. + Arguments inclusion [A] R1 R2. + Arguments preorder [A] R. Variable A : Type. Variable R : relation A. |