diff options
author | 2015-11-13 11:31:34 +0100 | |
---|---|---|
committer | 2015-11-13 11:31:34 +0100 | |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /test-suite/bugs/closed/4203.v | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
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 |