diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-03-11 10:32:14 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-03-11 10:36:17 +0100 |
commit | e9bf68016ce9e04feb63222ff4bbafd27531f564 (patch) | |
tree | 900e06e4cad2afd1084905f85de0fbe32dd9d2e6 /test-suite/bugs/closed/4588.v | |
parent | 4341f37cf3c51ed82c23f05846c8e6e8823d3cd6 (diff) |
According to Bruno, my fix for #4588 seems to be enough.
So adding a test-suite file and closing the bug.
Diffstat (limited to 'test-suite/bugs/closed/4588.v')
-rw-r--r-- | test-suite/bugs/closed/4588.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4588.v b/test-suite/bugs/closed/4588.v new file mode 100644 index 000000000..ff66277e0 --- /dev/null +++ b/test-suite/bugs/closed/4588.v @@ -0,0 +1,10 @@ +Set Primitive Projections. + +(* This proof was accepted in Coq 8.5 because the subterm specs were not +projected correctly *) +Inductive foo : Prop := mkfoo { proj1 : False -> foo; proj2 : (forall P : Prop, P -> P) }. + +Fail Fixpoint loop (x : foo) : False := + loop (proj2 x _ x). + +Fail Definition bad : False := loop (mkfoo (fun x => match x with end) (fun _ x => x)). |