From a9dc951e9068b18ee1cf0e51b2c4ae7a7c40354a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 May 2018 13:39:08 +0200 Subject: [ssr] implement {}/v as a short hand for {v}/v when v is an id --- test-suite/ssr/ipat_clear_if_id.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 test-suite/ssr/ipat_clear_if_id.v (limited to 'test-suite/ssr') 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. -- cgit v1.2.3