From cb1d2bfc2df6b9b8c6e1867a9ef28393f9f0c0f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Nov 2022 11:15:15 +0100 Subject: [PATCH] test --- apps/derive/tests/test_derive.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/apps/derive/tests/test_derive.v b/apps/derive/tests/test_derive.v index 5af5c9dd1..a4b4da763 100644 --- a/apps/derive/tests/test_derive.v +++ b/apps/derive/tests/test_derive.v @@ -168,3 +168,15 @@ Check Kwi _ (refl_equal 3). From Coq Require Ascii. #[only(param2)] derive Ascii.ascii. + +(* #407 *) +Definition is_zero (n:nat) := match n with O => true | _ => false end. +derive is_zero. + +Inductive toto1 := | Toto1 : forall n, unit -> is_zero n = true -> toto1. +Inductive toto2 := | Toto2 : forall n, is_zero n = true -> unit -> toto2. +Inductive toto3 := | Toto3 : unit -> forall n, is_zero n = true -> toto3. + +#[only(param1_trivial)] derive toto1. +#[only(param1_trivial)] derive toto2. +#[only(param1_trivial)] derive toto3.