1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
(*
This test is sensitive to changes in which let-ins are expanded when checking
for dependencies in constructors.
If the (x := X) is not reduced, Foo1 won't be recognized as a conjunction,
and if the (y := X) is reduced, Foo2 will be recognized as a conjunction.
This tests the behavior of engine/termops.ml : prod_applist_assum,
which is currently specified to reduce exactly the parameters.
If dtauto is changed to reduce lets in constructors before checking dependency,
this test will need to be changed.
*)
Parameter (P Q : Type).
Inductive Foo1 (X : Type) (x := X) := foo1 : let y := X in P -> Q -> Foo1 x.
Inductive Foo2 (X : Type) (x := X) := foo2 : let y := X in P -> Q -> Foo2 y.
Goal P -> Q -> Foo1 nat.
solve [dtauto].
Qed.
Goal P -> Q -> Foo2 nat.
Fail solve [dtauto].
Abort.
|
