From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- test-suite/bugs/closed/4203.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 test-suite/bugs/closed/4203.v (limited to 'test-suite/bugs/closed/4203.v') diff --git a/test-suite/bugs/closed/4203.v b/test-suite/bugs/closed/4203.v new file mode 100644 index 00000000..076a3c3d --- /dev/null +++ b/test-suite/bugs/closed/4203.v @@ -0,0 +1,19 @@ +Set Primitive Projections. + +Record ops {T:Type} := { is_ok : T -> Prop; constant : T }. +Arguments ops : clear implicits. + +Record ops_ok {T} (Ops:ops T) := { constant_ok : is_ok Ops (constant Ops) }. + +Definition nat_ops : ops nat := {| is_ok := fun n => n = 1; constant := 1 |}. +Definition nat_ops_ok : ops_ok nat_ops. +Proof. + split. cbn. apply eq_refl. +Qed. + +Definition t := Eval lazy in constant_ok nat_ops nat_ops_ok. +Definition t' := Eval vm_compute in constant_ok nat_ops nat_ops_ok. +Definition t'' := Eval native_compute in constant_ok nat_ops nat_ops_ok. + +Check (eq_refl t : t = t'). +Check (eq_refl t : t = t''). \ No newline at end of file -- cgit v1.2.3