remove special cases for CVC4 that are actually unused (see also 6273d4c8325b and 1f1c5d85d232);
authorwenzelm
Wed, 08 Jan 2025 14:35:30 +0100
changeset 81751 e4a2858ba7e2
parent 81750 377887fbc968
child 81752 a1743b71092e
remove special cases for CVC4 that are actually unused (see also 6273d4c8325b and 1f1c5d85d232);
src/HOL/Tools/Nunchaku/nunchaku.ML
src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Wed Jan 08 14:30:17 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Wed Jan 08 14:35:30 2025 +0100
@@ -277,9 +277,6 @@
               (print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE))
             | Nunchaku_Not_Found =>
               (print_n "External tool \"nunchaku\" not found"; (unknownN, NONE))
-            | CVC4_Cannot_Execute =>
-              (print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE))
-            | CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE))
             | Unknown_Error (code, msg) =>
               (print_n ("Error: " ^ unprefix_error msg ^
                  (if code = 0 then "" else " (code " ^ string_of_int code ^ ")"));
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Wed Jan 08 14:30:17 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Wed Jan 08 14:35:30 2025 +0100
@@ -33,8 +33,6 @@
   | Nunchaku_Var_Not_Set
   | Nunchaku_Cannot_Execute
   | Nunchaku_Not_Found
-  | CVC4_Cannot_Execute
-  | CVC4_Not_Found
   | Unknown_Error of int * string
 
   val nunchaku_home_env_var: string
@@ -70,8 +68,6 @@
 | Nunchaku_Var_Not_Set
 | Nunchaku_Cannot_Execute
 | Nunchaku_Not_Found
-| CVC4_Cannot_Execute
-| CVC4_Not_Found
 | Unknown_Error of int * string;
 
 val nunchaku_home_env_var = "NUNCHAKU_HOME";