diff options
Diffstat (limited to 'compiler/SymbolicToPure.ml')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 5252495d..5dc8664a 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2642,7 +2642,7 @@ let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression) let match_ty = body.ty in let match_e = Switch (fuel0, Match [ fail_branch; success_branch ]) in { e = match_e; ty = match_ty } - | Lean -> + | Lean | HOL4 -> (* We should have checked the command line arguments before *) raise (Failure "Unexpected") |