From 51b15993cb4a9cc2521b6107b7f4195b21040087 Mon Sep 17 00:00:00 2001 From: Xavier Clerc Date: Wed, 28 Jan 2015 14:26:19 +0100 Subject: Several reproduction cases for the test suite. --- test-suite/bugs/opened/3946.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/opened/3946.v (limited to 'test-suite/bugs/opened/3946.v') diff --git a/test-suite/bugs/opened/3946.v b/test-suite/bugs/opened/3946.v new file mode 100644 index 000000000..e77bdbc65 --- /dev/null +++ b/test-suite/bugs/opened/3946.v @@ -0,0 +1,11 @@ +Require Import ZArith. + +Inductive foo := Foo : Z.le 0 1 -> foo. + +Definition bar (f : foo) := let (f) := f in f. + +(* Doesn't work: *) +(* Arguments bar f.*) + +(* Does work *) +Arguments bar f _. -- cgit v1.2.3