From a0256a0012011ef685797c0bd4a92f6dd320f626 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 24 Jul 2007 15:04:12 +0000
Subject: fixed bug 1675: computing carrier from the relation type was not
 right

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10043 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/setoid_ring/Ring_tac.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 8a5aef564d..d5fc5f3485 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -145,8 +145,15 @@ Ltac ParseRingComponents lemma :=
 
 (* ring tactics *)
 
+Ltac relation_carrier req :=
+  let ty := type of req in
+  match eval hnf in ty with
+   ?R -> _ => R
+  | _ => fail 1000 "Equality has no relation type"
+  end.
+
 Ltac FV_hypo_tac mkFV req lH :=
-  let R := match type of req with ?R -> _ => R end in
+  let R := relation_carrier req in
   let FV_hypo_l_tac h :=
     match h with @mkhypo (req ?pe _) _ => mkFV pe end in
   let FV_hypo_r_tac h :=
-- 
cgit v1.2.3