From 5545969f485ef2fb944db8e7b0237acbabeb8d4c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 7 Sep 2010 08:28:07 -0400 Subject: Server-side 'onError' --- src/core_env.sml | 1 + 1 file changed, 1 insertion(+) (limited to 'src/core_env.sml') diff --git a/src/core_env.sml b/src/core_env.sml index 478ef495..9a4f9ec7 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -350,6 +350,7 @@ fun declBinds env (d, loc) = end | DTask _ => env | DPolicy _ => env + | DOnError _ => env fun patBinds env (p, loc) = case p of -- cgit v1.2.3