diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-12 11:35:08 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-27 13:28:01 +0200 |
commit | 18880888d56b3f5f1e69ddadb7aadf02b0c56401 (patch) | |
tree | 78db7878b0715491bff1c230ce0d2a140f722897 /test-suite | |
parent | ab84e2f45e2cdf99e5c69b90b628ef6618fe880a (diff) |
Test file for #7723
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/bugs/closed/7723.v | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v new file mode 100644 index 000000000..216290123 --- /dev/null +++ b/test-suite/bugs/closed/7723.v @@ -0,0 +1,58 @@ +Set Universe Polymorphism. + +Module Segfault. + +Inductive decision_tree : Type := . + +Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B + := match ls with + | nil => None + | cons x xs + => match f x with + | Some v => Some v + | None => first_satisfying_helper f xs + end + end. + +Axiom admit : forall {T}, T. +Definition dtree4 : option decision_tree := + match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil) + with + | Some _ => admit + | None => admit + end +. +Definition dtree'' := Eval vm_compute in dtree4. (* segfault *) + +End Segfault. + +Module OtherExample. + +Definition bar@{i} := Type@{i}. +Definition foo@{i j} (x y z : nat) := + @id Type@{j} bar@{i}. +Eval vm_compute in foo. + +End OtherExample. + +Module LocalClosure. + +Definition bar@{i} := Type@{i}. + +Definition foo@{i j} (x y z : nat) := + @id (nat -> Type@{j}) (fun _ => Type@{i}). +Eval vm_compute in foo. + +End LocalClosure. + +Require Import Hurkens. +Polymorphic Inductive unit := tt. + +Polymorphic Definition foo := + let x := id tt in (x, x, Type). + +Lemma bad : False. + refine (TypeNeqSmallType.paradox (snd foo) _). + vm_compute. + Fail reflexivity. +Abort. |