(* f1 was renamed into Coq__1.f1 but Coq__1 was not defined *) (* similar to #12813, #16677 *)
Record r : Type := mk { f1 : unit -> unit; f2: unit -> unit }. Set Primitive Projections.
Record r' : Type := mk' { f1' : unit -> unit; f2': unit -> unit }. Unset Primitive Projections.
Module M. Definition f1 (ti:unit) : unit := tt. Definition f2 (ti:unit) : unit := tt. Definition cf := mk f1 f2.
Definition f1' (ti:unit) : unit := tt. Definition f2' (ti:unit) : unit := tt. Definition cf' := mk' f1' f2'. End M.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
