Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale sprachen/Coq/test-suite/bugs/closed/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_5598.v Sprache: Coq

Untersuchung Coq^©

Module Type TA.
Parameter t : Set.
End TA.

Module Type TB.
Declare Module A: TA.
End TB.

Module Type TC.
Declare Module B : TB.
End TC.

Module Type TD.

Declare Module B: TB .
Declare Module C: TC
    with Module B := B  .
End TD.

Module Type TE.
Declare Module D : TD.
End TE.

Module Type TF.
Declare Module E:  TE.
End TF.

Module G (D: TD).
Module B' := D.C.B.
End G.

Module H  (F: TF).
Module I := G(F.E.D).
End H.

Declare Module F:  TF.
Module K := H(F).