From c6de35c598c9d0a02ebbd5209891cafc0268e4ed Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Fri, 30 Apr 2021 00:07:19 +0200
Subject: [PATCH 1/2] Add coverage for the constants

---
 tests/constants.ml | 13 +++++++++++++
 tests/constants.v  | 24 ++++++++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 tests/constants.ml
 create mode 100644 tests/constants.v

diff --git a/tests/constants.ml b/tests/constants.ml
new file mode 100644
index 000000000..c54b379df
--- /dev/null
+++ b/tests/constants.ml
@@ -0,0 +1,13 @@
+let c_int : int = 0
+
+let c_char : char = 'c'
+
+let c_string : string = "c"
+
+let c_float : float = 1.0
+
+let c_int32 : int32 = 0l
+
+let c_int64 : int64 = 0L
+
+let c_nativeint : nativeint = 0n
diff --git a/tests/constants.v b/tests/constants.v
new file mode 100644
index 000000000..6008341e4
--- /dev/null
+++ b/tests/constants.v
@@ -0,0 +1,24 @@
+Require Import CoqOfOCaml.CoqOfOCaml.
+Require Import CoqOfOCaml.Settings.
+
+Definition c_int : int := 0.
+
+Definition c_char : ascii := "c" % char.
+
+Definition c_string : string := "c".
+
+Definition c_float : float :=
+  (* ❌ Float constant 1.0 is approximated by the integer 1 *)
+  1.
+
+Definition c_int32 : int32 :=
+  (* ❌ Constant of type int32 is converted to int *)
+  0.
+
+Definition c_int64 : int64 :=
+  (* ❌ Constant of type int64 is converted to int *)
+  0.
+
+Definition c_nativeint : nativeint :=
+  (* ❌ Constant of type nativeint is converted to int *)
+  0.

From b364d583a5e721071a7fe3d1ac34b7cdb60c357a Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Fri, 30 Apr 2021 16:31:33 +0200
Subject: [PATCH 2/2] Catch the exceptions with a nicer error message

---
 src/coqOfOCaml.ml | 14 ++++++++++----
 src/error.ml      |  3 ++-
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/coqOfOCaml.ml b/src/coqOfOCaml.ml
index 74bab2eb2..e7db45568 100644
--- a/src/coqOfOCaml.ml
+++ b/src/coqOfOCaml.ml
@@ -101,13 +101,13 @@ let of_ocaml
     success_message;
   }
 
-let exit (context : MonadEval.Context.t) (output : Output.t) : unit =
+let get_exit_code (context : MonadEval.Context.t) (output : Output.t) : int =
   let is_blacklist =
     Configuration.is_filename_in_error_blacklist context.configuration in
   if output.has_errors && not is_blacklist then
-    exit 1
+    1
   else
-    exit 0
+    0
 
 (** The main function. *)
 let main () =
@@ -163,6 +163,7 @@ let main () =
     let pipeline = Mpipeline.make merlin_config file_source in
 
     Mpipeline.with_pipeline pipeline (fun _ ->
+      try
         let comments = Mpipeline.reader_comments pipeline in
         let typing = Mpipeline.typer_result pipeline in
         let typedtree = Mtyper.get_typedtree typing in
@@ -183,6 +184,11 @@ let main () =
             !output_file_name
             !json_mode in
         Output.write !json_mode output;
-        exit context output)
+        let exit_code = get_exit_code context output in
+        exit exit_code
+      with Failure message ->
+        prerr_endline message;
+        exit 1
+    )
 
 ;;main ()
diff --git a/src/error.ml b/src/error.ml
index 746277e1d..7c4322d85 100644
--- a/src/error.ml
+++ b/src/error.ml
@@ -1,4 +1,5 @@
-(** Error messages. *)
+(** Error messages. We handle the errors with a monad, and allopw multiple
+    errors per file. *)
 open SmartPrint
 
 module Category = struct