diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-08-22 08:32:59 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-09-28 15:41:45 +0200 |
| commit | 8e0f29cb69f06b64d74b18b09fb6a717034f1140 (patch) | |
| tree | e64020b49acb7275e3609614bc171127c04405eb /test-suite/success/bteauto.v | |
| parent | 405acea72a67c31ec8554c1f76d51518a5df769a (diff) | |
Typeclass backtracking example by J. Leivant
Diffstat (limited to 'test-suite/success/bteauto.v')
| -rw-r--r-- | test-suite/success/bteauto.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 590f6e191..bb1cf0654 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. |