From 6fabdb398ffedd3f3ffdef3cd02b8749be20445b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 16 Dec 2008 10:19:06 +0000
Subject: Finish fix for the treatment of [inverse] in [setoid_rewrite], making
 a variant of the [unify] tactic that takes a hint db as argument and does
 unification modulo its [transparent_state]. Add test-file for bug #1939 and
 another [AdvancedTypeClasses.v] that mimicks [AdvancedCanonicalStructure.v].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11685 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Classes/Init.v    | 2 +-
 theories/Program/Tactics.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories')

diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 8b4cac5f4e..7fb48aa433 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -33,7 +33,7 @@ Class Unconvertible (A : Type) (a b : A).
 
 Ltac unconvertible :=
   match goal with
-    | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible"
+    | |- @Unconvertible _ ?x ?y => unify x y with typeclass_instances ; fail 1 "Convertible"
     | |- _ => eapply Build_Unconvertible 
   end.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index eb5c7cc11f..fff78a85af 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -93,7 +93,7 @@ Ltac clear_dup :=
         | [ H' : ?Y |- _ ] =>
           match H with
             | H' => fail 2
-            | _ => conv X Y ; (clear H' || clear H)
+            | _ => unify X Y ; (clear H' || clear H)
           end
       end
   end.
-- 
cgit v1.2.3