Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_4484.v Sprache: Coq

Original von: Coq^©

(** Namespace of module vs. namescope of definitions/constructors/...

As noticed by A. Appel in bug #2603, module names and definition
names used to be in the same namespace. But conflict with names
of constructors (or 2nd mutual inductive...) used to not be checked
enough, leading to strange situations.

- In 8.3pl3 we introduced checks that forbid uniformly the following
  situations.

- For 8.4 we finally managed to make module names and other names
  live in two separate namespace, hence allowing all of the following
  situations.
*)

Module Type T.
End T.

Declare Module K : T.

Module Type L.
Declare Module E : T.
End L.

Module M1 : L with Module E:=K.
Module E := K.
Inductive t := E. (* Used to be accepted, but End M1 below was failing *)
End M1.

Module M2 : L with Module E:=K.
Inductive t := E.
Module E := K. (* Used to be accepted *)
End M2. (* Used to be accepted *)

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.