From 8e0f29cb69f06b64d74b18b09fb6a717034f1140 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 22 Aug 2016 08:32:59 +0200
Subject: Typeclass backtracking example by J. Leivant

---
 test-suite/success/bteauto.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 590f6e191f..bb1cf06541 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -46,6 +46,25 @@ Module Backtracking.
   Qed.
   
   Unset Typeclasses Debug.
+
+  Module Leivant.
+    Axiom A : Type.
+    Existing Class A.
+    Axioms a b c d e: A.
+    
+    Ltac get_value H := eval cbv delta [H] in H.
+    
+    Goal True.
+      Fail refine (let H := _ : A in _); let v := get_value H in idtac v; fail.
+    Admitted.
+
+    Goal exists x:A, x=a.
+      unshelve evar (t : A). all:cycle 1.
+      refine (@ex_intro _ _ t _).
+      all:cycle 1.
+      all:(typeclasses eauto + reflexivity).
+    Qed.      
+  End Leivant.
 End Backtracking.
 
 
-- 
cgit v1.2.3