1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v
index 976bec73..e25510cf 100644
--- a/test-suite/success/clear.v
+++ b/test-suite/success/clear.v
@@ -13,3 +13,21 @@ Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True.
   reflexivity.
 Qed.
 
+Class A.
+
+Section Foo.
+
+  Variable a : A.
+
+  Goal A.
+    solve [typeclasses eauto].
+    Undo 1.
+    clear a.
+    try typeclasses eauto.
+    assert(a:=Build_A).
+    solve [ typeclasses eauto ].
+    Undo 2.
+    assert(b:=Build_A).
+    solve [ typeclasses eauto ].
+  Qed.
+End Foo.
+\ No newline at end of file