diff options
Diffstat (limited to 'test-suite/bugs/closed/4203.v')
-rw-r--r-- | test-suite/bugs/closed/4203.v | 19 |
1 files changed, 19 insertions, 0 deletions
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 |