From 86f12419f2c89500aa380e2e29cfffd309758201 Mon Sep 17 00:00:00 2001 From: Abdelghani ALIDRA Date: Tue, 9 Apr 2024 12:44:04 +0200 Subject: [PATCH] add square brakets to location message when object is not found --- src/parsing/scope.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index fc84ac650..279b68f17 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -512,9 +512,9 @@ let scope_term : let md = M_Term {m_term_meta_of_key=mok; m_term_prv} in Bindlib.unbox (scope ?find_sym ~typ 0 md ss env t) with Fatal(Some p, msg) -> - Console.out 3 (Color.red "%a") Pos.pp p; + Console.out 3 (Color.red "[%a]") Pos.pp p; (** Get ride of the position because the error message is displayed here - There is no more need of the position and this avoids the message + There is no more need of the position and this avoids the message to be displayed twice in [Error.handle_exceptions] *) raise(Fatal(None, msg))