From 2face8d77628ded64f7d0a824f4b377694b9d7fd Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 6 Jul 2015 15:22:20 +0200 Subject: Test case for #4203, fixed by commit a51cce36. --- 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') diff --git a/test-suite/bugs/closed/4203.v b/test-suite/bugs/closed/4203.v new file mode 100644 index 000000000..076a3c3d6 --- /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