diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index e15f69a97..fc84ac650 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -508,8 +508,15 @@ let scope_term :
       ?find_sym:find_sym -> ?typ:bool -> ?mok:(int -> meta option)
       -> bool -> sig_state -> env -> p_term -> term =
   fun ?find_sym ?(typ=false) ?(mok=fun _ -> None) m_term_prv ss env t ->
-  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)
+  try
+    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;
+    (**  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 
+        to be displayed twice in [Error.handle_exceptions] *)
+    raise(Fatal(None,    msg))
 
 (** [scope_search_pattern ~find_sym ~typ prv ss env t] turns a pterm [t] meant
     to be a search patter into a term in the signature state [ss]