From 02029b85488b0e8e1831810aa16d53626c418270 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 10 Jun 2009 03:59:02 +0000
Subject: Use the projections for reflexivity, symmetry and transitivity proofs
 to ensure the type and relation used in the subgoals stay syntactically the
 same, for compatibility with [ring] which does not use conversion to find the
 ring on a relation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12179 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 4eccf41cac..213dcc8d21 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -217,7 +217,8 @@ let proper_proof env evars carrier relation x =
 let find_class_proof proof_type proof_method env evars carrier relation =
   try 
     let goal = mkApp (Lazy.force proof_type, [| carrier ; relation |]) in
-      Typeclasses.resolve_one_typeclass env evars goal
+    let c = Typeclasses.resolve_one_typeclass env evars goal in
+      mkApp (Lazy.force proof_method, [| carrier; relation; c |])
   with e when Logic.catchable_exception e -> raise Not_found
 
 let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
-- 
cgit v1.2.3