The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

(* You can still sort of do it a la Instance with the refine tactic. *)

Record A := {
 num: nat
}.

Record B := {
 base : A;
 e: num base > 2
}.

Definition A_Sample: A := {| num := 3 |}.

Definition B_Sample : B.
Proof.
  refine {| base := A_Sample |}.
  auto.
Qed.