From 35c6b1c3c3dbd1b782cb00206c773021f5c74765 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 14:32:19 +0200
Subject: Add an option to run Aeneas as a borrow checker

---
 compiler/PureUtils.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/PureUtils.ml')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index e7dcd933..fe5d3414 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -241,7 +241,7 @@ let rec let_group_requires_parentheses (span : Meta.span) (e : texpression) :
         msg (* TODO : check if true should'nt be returned instead ? *)
 
 let texpression_requires_parentheses span e =
-  match !Config.backend with
+  match Config.backend () with
   | FStar | Lean -> false
   | Coq | HOL4 -> let_group_requires_parentheses span e
 
-- 
cgit v1.2.3