Skip to content
Snippets Groups Projects
Commit 640df815 authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

The MC.tla no longer extends TLC.tla to prevent name clashes with user 

defined operators. If no user defined PrintT or Print operator exists
and TLC is *not* explicitly extended, local definitions of PrintT and
Print will be added to the MC file (for backward compatibility and to
support evaluation of constant expressions).

See related commit 5249fa51

Fixes Github issue #103
https://github.com/tlaplus/tlaplus/issues/103

[Bug][Toolbox][Changelog]
parent 5249fa51
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment