1 files changed, 26 insertions, 0 deletions
diff --git a/mathcomp/ssrtest/deferclear.v b/mathcomp/ssrtest/deferclear.v
new file mode 100644
index 0000000..a13a20e
--- /dev/null
+++ b/mathcomp/ssrtest/deferclear.v
@@ -0,0 +1,26 @@
+(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import ssreflect.
+Require Import ssrbool eqtype fintype ssrnat.
+
+Variable T : Type.
+
+Lemma test0 : forall a b c d : T, True.
+Proof. by move=> a b {a} a c; exact I. Qed.
+
+Variable P : T -> Prop.
+
+Lemma test1 : forall a b c : T, P a -> forall d : T, True.
+Proof. move=> a b {a} a _ d; exact I. Qed.
+
+Definition Q := forall x y : nat, x = y.
+Axiom L : 0 = 0 -> Q.
+Axiom L' : 0 = 0 -> forall x y : nat, x = y.
+Lemma test3 : Q.
+by apply/L.
+Undo.
+rewrite /Q.
+by apply/L.
+Undo 2.
+by apply/L'.
+Qed.
+