From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 theories/Classes/Init.v | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'theories/Classes/Init.v')

diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 6ba0c61e..e5f951d0 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -13,9 +13,22 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Init.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: Init.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 (* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
 
 Tactic Notation "clapply" ident(c) :=
   eapply @c ; eauto with typeclass_instances.
+
+(** The unconvertible typeclass, to test that two objects of the same type are 
+   actually different. *)
+
+Class Unconvertible (A : Type) (a b : A).
+
+Ltac unconvertible :=
+  match goal with
+    | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible"
+    | |- _ => apply Build_Unconvertible 
+  end.
+
+Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file
-- 
cgit v1.2.3