From 8082d1faf85a0ab29f6c144a137791902a4e9c1f Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 5 Oct 2011 15:51:57 +0000 Subject: Fixing critical inductive polymorphism bug found by Bruno. If two distinct parameters of the inductive type contributes to polymorphism, they must have distinct names, othewise an aliasing problem of the form "fun x x => max(x,x)" happens. Also insisted that a parameter contributes to universe polymorphism only if the corresponding occurrence of Type is not hidden behind a definition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/failure/inductive4.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 test-suite/failure/inductive4.v (limited to 'test-suite/failure') diff --git a/test-suite/failure/inductive4.v b/test-suite/failure/inductive4.v new file mode 100644 index 000000000..6ba36fd20 --- /dev/null +++ b/test-suite/failure/inductive4.v @@ -0,0 +1,15 @@ +(* This used to succeed in versions 8.1 to 8.3 *) + +Require Import Logic. +Require Hurkens. +Definition Ti := Type. +Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y. +Definition B : Prop := let F := prod True in F Prop. (* Aie! *) +Definition p2b (P:Prop) : B := pair True Prop I P. +Definition b2p (b:B) : Prop := match b with pair _ P => P end. +Lemma L1 : forall A : Prop, b2p (p2b A) -> A. +Proof (fun A x => x). +Lemma L2 : forall A : Prop, A -> b2p (p2b A). +Proof (fun A x => x). +Check Hurkens.paradox B p2b b2p L1 L2. + -- cgit v1.2.3