diff options
| author | Pierre-Marie Pédrot | 2018-11-05 11:59:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-05 11:59:27 +0100 |
| commit | 62c75af6595fc31ec076b1bedfae62f652eda05e (patch) | |
| tree | d53a1ab493043f4a0cb46d675e81bd5f1ead401d /test-suite | |
| parent | 3c8e41cb39647b8d8cd6cb9ecd6bb887a3aedfb7 (diff) | |
| parent | 6da464438366b2b5d752b44536b2bedac2a34187 (diff) | |
Merge PR #8874: Fix #8873: coqchk on inductive with letin parameter
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/coqchk/bug_8655.v | 1 | ||||
| -rw-r--r-- | test-suite/success/Inductive.v | 2 |
2 files changed, 1 insertions, 2 deletions
diff --git a/test-suite/coqchk/bug_8655.v b/test-suite/coqchk/bug_8655.v new file mode 100644 index 0000000000..06d08b2082 --- /dev/null +++ b/test-suite/coqchk/bug_8655.v @@ -0,0 +1 @@ +Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2). diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index f07c0191f1..c2130995fc 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -1,7 +1,5 @@ (* Test des definitions inductives imbriquees *) -Require Import List. - Inductive X : Set := cons1 : list X -> X. |