summaryrefslogtreecommitdiff
path: root/compiler/PureUtils.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/PureUtils.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 1f5d1ed8..9b768f3b 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -169,7 +169,7 @@ let rec let_group_requires_parentheses (e : texpression) : bool =
let texpression_requires_parentheses e =
match !Config.backend with
| FStar | Lean -> false
- | Coq -> let_group_requires_parentheses e
+ | Coq | HOL4 -> let_group_requires_parentheses e
let is_var (e : texpression) : bool =
match e.e with Var _ -> true | _ -> false