diff options
| author | Hugo Herbelin | 2020-12-06 03:03:12 +0100 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2021-04-04 18:01:25 +0900 |
| commit | a265c1ad912b4940861ec27efd09e5b20d33233c (patch) | |
| tree | 7e6e189371a252b9e51aff09105c49b1e6cf0f96 /test-suite | |
| parent | 012b8a08f142d39b2211fd52c811f830f88f2075 (diff) | |
Fixing #13581: missing support for let-ins in arity of inductive types.
At first view, the fix takes care about when to use the number of
assumptions and when to also include local definitions, but I don't
know all the details of the implementation to be absolutely sure.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_13581.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13581.v b/test-suite/bugs/closed/bug_13581.v new file mode 100644 index 0000000000..9f129f331e --- /dev/null +++ b/test-suite/bugs/closed/bug_13581.v @@ -0,0 +1,6 @@ +From Coq Require Extraction. + +Record mixin_of T0 (b : unit) (T := T0) := Mixin { _ : T0 -> let U:=T0 in U }. +Definition d := Mixin nat tt (fun x => x). + +Extraction TestCompile d. |