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

1 files changed, 13 insertions, 12 deletions

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).