Convert OOME / DebugE / UBE to using print_msg.

vellvm · Jul 3, 2023 · b954bbd · b954bbd
1 parent 3ca4571
commit b954bbd
Show file tree

Hide file tree

Showing 8 changed files with 5,232 additions and 3,327 deletions.
diff --git a/src/coq/Handlers/OOM.v b/src/coq/Handlers/OOM.v
@@ -300,7 +300,7 @@ Section PARAMS_INTERP.
   Notation Effout := (E +' OOME +' F).
 
   Definition OOM_exec_fail {E} `{FailureE -< E}: OOME ~> itree E :=
-    fun _ e => match e with | ThrowOOM s => raise ("Abort (OOM): " ++ s) end.
+    fun _ e => match e with | ThrowOOM tt => raise ("Abort (OOM)") end.
 
   Definition OOM_exec {E} `{OOME -< E} : OOME ~> itree E :=
     fun R e => trigger e.