Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: objects2.v Sprache: Coq

Original von: Coq^©

(* Check that non logical object loading is done after registration of
   the logical objects in the environment
*)

(* BZ#1118 (simplified version), submitted by Evelyne Contejean
  (used to failed in pre-V8.1 trunk because of a call to lookup_mind
   for structure objects)
*)

Module Type S. Record t : Set := { a : nat; b : nat }. End S.
Module Make (X:S). Module Y:=X. End Make.

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.