From 2fed21d8767eb05972e165256ed22f98feed59c6 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 14 Feb 2012 14:35:51 +0000
Subject: In [reflexivity], [symmetry] etc, use the type found by looking at
 the relation as the carrier instead of the first argument's type (plays nicer
 with coercions).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14979 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/rewrite.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1cc1b27fe0..ef3ec14702 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1867,7 +1867,8 @@ let setoid_proof gl ty fn fallback =
   let env = pf_env gl in
     try
       let rel, args = decompose_app_rel env (project gl) (pf_concl gl) in
-      let evm, car = project gl, pf_type_of gl args.(0) in
+      let evm = project gl in
+      let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
 	fn env evm car rel gl
     with e ->
       try fallback gl
-- 
cgit v1.2.3