From 10fa6e15b6aa7c398041167983f643f6c1de001c Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 13 Oct 2009 20:37:53 +0000 Subject: Made implicit arguments of Operators_Properties.v local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12387 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Operators_Properties.v | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index c17f5f64e..b3f30ddf2 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -18,19 +18,20 @@ Require Import Relation_Definitions. Require Import Relation_Operators. Require Import Setoid. -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]. - 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]. + Variable A : Type. Variable R : relation A. @@ -40,7 +41,7 @@ Section Properties. (** Correctness of the reflexive-transitive closure operator *) - Lemma clos_rt_is_preorder : preorder A (clos_refl_trans R). + Lemma clos_rt_is_preorder : preorder R*. Proof. apply Build_preorder. exact (rt_refl A R). -- cgit v1.2.3