diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/language/l2.ott b/language/l2.ott index c34dedb5..a437f915 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -230,9 +230,7 @@ base_effect :: 'BE_' ::= | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} - | escape :: :: escape {{ com potential call of $[[exit]]$ }} - | lset :: :: lset {{ com local mutation; not user-writable }} - | lret :: :: lret {{ com local return; not user-writable }} + | escape :: :: escape {{ com potential exception }} effect :: 'Effect_' ::= {{ com effect set, of kind $[[Effect]]$ }} |