Merge pull request #258 from ejgallego/v8.13+fix_412_warn

[build] Remove 4.12 warnings, test 4.12 in the CI
rocq-archive · Sep 22, 2021 · 2f557aa · 2f557aa
2 parents f5c7ff6 + b7eb4b4
commit 2f557aa
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 5 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -25,7 +25,7 @@ jobs:
   build:
     strategy:
       matrix:
-        ocaml-version: [4.07.1, 4.08.1, 4.09.1, 4.10.1, 4.11.1]
+        ocaml-version: [4.07.1, 4.08.1, 4.09.1, 4.10.1, 4.11.1, 4.12.0]
         test-target: [test]
         extra-opam: ["coq.8.13.0 coq-mathcomp-ssreflect"]
         include:

diff --git a/CHANGES.md b/CHANGES.md
@@ -17,6 +17,7 @@
             @ejgallego, reported by @cpitclaudel)
  - [sertop] New option `--omit_env` that will disable the serialization of
             Coq's super heavy global environments (#254 @ejgallego)
+ - [build]  Test OCaml 4.12 (#257 @ejgallego)
 
 ## Version 0.13.0:
 

diff --git a/serapi/serapi_doc.ml b/serapi/serapi_doc.ml
@@ -29,7 +29,7 @@ let check_pending_proofs ~pstate =
     CErrors.user_err msg
     ) pstate
 
-let save_vo ~doc ?ldir ~pstate ~in_file =
+let save_vo ~doc ?ldir ~pstate ~in_file () =
   let _doc = Stm.join ~doc in
   check_pending_proofs ~pstate;
   let ldir = match ldir with

diff --git a/serapi/serapi_doc.mli b/serapi/serapi_doc.mli
@@ -23,3 +23,4 @@ val save_vo
   -> pstate:Declare.Proof.t option
   -> in_file:string
   -> unit
+  -> unit
diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml
@@ -908,7 +908,7 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t =
         let _doc = Stm.observe ~doc opts.sid in
         let pst = Stm.state_of_id ~doc opts.sid in
         let pstate = pstate_of_st pst in
-        Serapi_doc.save_vo ~doc ~pstate ~in_file ?ldir:st.ldir; []
+        Serapi_doc.save_vo ~doc ~pstate ~in_file ?ldir:st.ldir (); []
     end
   | Add (opt, s) ->
     let _doc, pa, res = ControlUtil.add_sentences ~doc opt s in

diff --git a/sertop/sertop_sexp.ml b/sertop/sertop_sexp.ml
@@ -84,7 +84,7 @@ module Ctx = struct
     ; st : SP.State.t
     }
 
-  let make ?in_file ?ldir ~cmd_id ~in_chan ~out_chan =
+  let make ?in_file ?ldir ~cmd_id ~in_chan ~out_chan () =
     let out_fmt = Format.formatter_of_out_channel out_chan in
     let st = SP.State.make ?in_file ?ldir () in
     { out_chan; out_fmt; in_chan; cmd_id; st }
@@ -207,7 +207,7 @@ let ser_loop ser_opts =
 
   let ldir = Option.map Serapi.Serapi_paths.dirpath_of_file ser_opts.topfile in
   let ctx = Ctx.make
-      ?in_file:ser_opts.topfile ?ldir ~cmd_id:0 ~in_chan:ser_opts.in_chan ~out_chan:ser_opts.out_chan  in
+      ?in_file:ser_opts.topfile ?ldir ~cmd_id:0 ~in_chan:ser_opts.in_chan ~out_chan:ser_opts.out_chan () in
 
   (* Init Coq *)
   let () = Sertop_init.(
-Original file line number
+Diff line change
@@ Expand Up / @@ -23,3 +23,4 @@ val save_vo @@
       -> pstate:Declare.Proof.t option
       -> in_file:string
       -> unit
+      -> unit