From a2bb6f5358df6be7f1089a1a06feaf42a6c81257 Mon Sep 17 00:00:00 2001 From: xclerc Date: Fri, 20 Sep 2013 13:28:06 +0000 Subject: Fix name clash in "failure/inductive.v". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16800 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/failure/inductive.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'test-suite/failure') diff --git a/test-suite/failure/inductive.v b/test-suite/failure/inductive.v index 143e8bb36..f3e47bfd2 100644 --- a/test-suite/failure/inductive.v +++ b/test-suite/failure/inductive.v @@ -15,10 +15,10 @@ Fail Inductive u : Type := d : u | e : t u -> u. Require Import Logic. Require Hurkens. Definition Ti := Type. -Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y. -Fail 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. +Inductive prod2 (X Y:Ti) := pair2 : X -> Y -> prod2 X Y. +Fail Definition B : Prop := let F := prod2 True in F Prop. (* Aie! *) +(*Definition p2b (P:Prop) : B := pair2 True Prop I P. +Definition b2p (b:B) : Prop := match b with pair2 _ 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). -- cgit v1.2.3