From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/1683.v | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 test-suite/bugs/closed/1683.v (limited to 'test-suite/bugs/closed/1683.v') diff --git a/test-suite/bugs/closed/1683.v b/test-suite/bugs/closed/1683.v new file mode 100644 index 00000000..3e99694b --- /dev/null +++ b/test-suite/bugs/closed/1683.v @@ -0,0 +1,42 @@ +Require Import Setoid. + +Section SetoidBug. + +Variable ms : Type. +Variable ms_type : ms -> Type. +Variable ms_eq : forall (A:ms), relation (ms_type A). + +Variable CR : ms. + +Record Ring : Type := +{Ring_type : Type}. + +Variable foo : forall (A:Ring), nat -> Ring_type A. +Variable IR : Ring. +Variable IRasCR : Ring_type IR -> ms_type CR. + +Definition CRasCRing : Ring := Build_Ring (ms_type CR). + +Hypothesis ms_refl : forall A x, ms_eq A x x. +Hypothesis ms_sym : forall A x y, ms_eq A x y -> ms_eq A y x. +Hypothesis ms_trans : forall A x y z, ms_eq A x y -> ms_eq A y z -> ms_eq A x z. + +Add Parametric Relation A : (ms_type A) (ms_eq A) + reflexivity proved by (ms_refl A) + symmetry proved by (ms_sym A) + transitivity proved by (ms_trans A) + as ms_Setoid. + +Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n). + +Goal forall (b:ms_type CR), + ms_eq CR (IRasCR (foo IR O)) b -> + ms_eq CR (IRasCR (foo IR O)) b. +intros b H. +rewrite foobar. +rewrite foobar in H. +assumption. +Qed. + + + -- cgit v1.2.3