From cc03c37b48af466e6673fa4cb034e6ef19f709c0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Oct 2017 19:11:48 +0200
Subject: [stdlib] Fix warnings on deprecated `Add Setoid`

The test suite cases are preserved until the feature is actually removed.
---
 test-suite/bugs/closed/1322.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/1322.v b/test-suite/bugs/closed/1322.v
index 1ec7d452a6..6941ade44c 100644
--- a/test-suite/bugs/closed/1322.v
+++ b/test-suite/bugs/closed/1322.v
@@ -12,7 +12,11 @@ Variable I_eq_equiv : Setoid_Theory I I_eq.
   transitivity proved by I_eq_equiv.(Seq_trans I I_eq)
 as I_eq_relation. *)
 
-Add Setoid I I_eq I_eq_equiv as I_with_eq.
+Add Parametric Relation : I I_eq
+  reflexivity  proved by I_eq_equiv.(@Equivalence_Reflexive _ _)
+  symmetry     proved by I_eq_equiv.(@Equivalence_Symmetric _ _)
+  transitivity proved by I_eq_equiv.(@Equivalence_Transitive _ _)
+  as I_with_eq.
 
 Variable F : I -> Type.
 Variable F_morphism : forall i j, I_eq i j -> F i = F j.
-- 
cgit v1.2.3