From 99aa9904cb19255a154937a0cca39fbc536ffe97 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Sep 2010 10:18:01 +0000
Subject: Patch solving the bug but leaving open design choices

The patch does not address the possible use of evars by get_symmetric_proof in
unify_eqn. Someting has still to be done there.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13435 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/setoid_ring/newring.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index fa0e76841a..e625fe3b4e 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -455,9 +455,9 @@ let setoid_of_relation env a r =
   try
     lapp coq_mk_Setoid
       [|a ; r ;
-	Rewrite.get_reflexive_proof env evm a r ;
-	Rewrite.get_symmetric_proof env evm a r ;
-	Rewrite.get_transitive_proof env evm a r |]
+	fst (Rewrite.get_reflexive_proof env evm a r) ;
+	fst (Rewrite.get_symmetric_proof env evm a r) ;
+	fst (Rewrite.get_transitive_proof env evm a r) |]
   with Not_found ->
     error "cannot find setoid relation"
 
-- 
cgit v1.2.3