From 53b6f555a5068f3ded38c623f1939e082b3268ae Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Mon, 23 Nov 2020 17:53:17 +0100
Subject: fixing [dup] for Coq 8.12

---
 mathcomp/test_suite/test_intro_rw.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'mathcomp/test_suite')

diff --git a/mathcomp/test_suite/test_intro_rw.v b/mathcomp/test_suite/test_intro_rw.v
index dd1486f..827b810 100644
--- a/mathcomp/test_suite/test_intro_rw.v
+++ b/mathcomp/test_suite/test_intro_rw.v
@@ -21,3 +21,27 @@ Proof.
 move=> /[apply] b.
 Check (b : B).
 Abort.
+
+Lemma test_swap_plus P Q : P -> Q -> False.
+Proof.
+move=> + /[dup] q.
+suff: P -> Q -> False by [].
+Abort.
+
+Lemma test_dup_plus2 P : P -> let x := 0 in False.
+Proof.
+move=> + /[dup] y.
+suff: P -> let x := 0 in False by [].
+Abort.
+
+Lemma test_swap_plus P Q R : P -> Q -> R -> False.
+Proof.
+move=> + /[swap].
+suff: P -> R -> Q -> False by [].
+Abort.
+
+Lemma test_swap_plus2 P : P -> let x := 0 in let y := 1 in False.
+Proof.
+move=> + /[swap].
+suff: P -> let y := 1 in let x := 0 in False by [].
+Abort.
-- 
cgit v1.2.3