(* These tests are only about a subset of #7068 *) (* The original issue is still open *)
Inductive foo : let T := Type in T := . Definition bob1 := Eval vm_compute in foo_rect. Definition bob2 := Eval native_compute in foo_rect. Definition bob3 := Eval lazy in foo_rect.
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.
