From 33789b2d1706194d478a25098bd1991d2c845223 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 27 Nov 2017 19:18:21 +0100
Subject: [error] Replace msg_error by a proper exception.

The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.

As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
---
 engine/logic_monad.ml  | 1 -
 engine/logic_monad.mli | 1 -
 2 files changed, 2 deletions(-)

(limited to 'engine')

diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 9dc5d473b9..3674bb9432 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -107,7 +107,6 @@ struct
   let print_debug   s = make (fun _ -> Feedback.msg_info s)
   let print_info    s = make (fun _ -> Feedback.msg_info s)
   let print_warning s = make (fun _ -> Feedback.msg_warning s)
-  let print_error   s = make (fun _ -> Feedback.msg_error s)
   let print_notice  s = make (fun _ -> Feedback.msg_notice s)
 
   let run = fun x ->
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 8c8f9fe935..50b4abd8bd 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -61,7 +61,6 @@ module NonLogical : sig
   val print_warning : Pp.t -> unit t
   val print_notice : Pp.t -> unit t
   val print_info : Pp.t -> unit t
-  val print_error : Pp.t -> unit t
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
-- 
cgit v1.2.3