aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-23 17:09:47 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-23 17:09:47 +0200
commit7836f9319f17a642921cbf9b153077fc195ca8e1 (patch)
tree70dc89c80436adcfde89e2c0a02cf5163fb77266 /test-suite
parentddd99ca6b4a23286405ec995379e4b07d42b0f78 (diff)
parentdb2147fe29ca5d805f94e1a61f8a568dcd9b620f (diff)
Merge PR #7236: [ssr] simpler semantics for delayed clears
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/ssr/ipat_clear_if_id.v23
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v
new file mode 100644
index 000000000..7a44db2ea
--- /dev/null
+++ b/test-suite/ssr/ipat_clear_if_id.v
@@ -0,0 +1,23 @@
+Require Import ssreflect.
+
+Axiom v1 : nat -> bool.
+
+Section Foo.
+
+Variable v2 : nat -> bool.
+
+Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True.
+Proof.
+move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4.
+Check b1 : bool.
+Check b2 : bool.
+Check b3 : bool.
+Check b4 : bool.
+Fail Check v3.
+Fail Check v4.
+Fail Check v5.
+Check v2 : nat -> bool.
+by [].
+Qed.
+
+End Foo.