[port] Bump serapi to 0.15.0.

.gitmodules

@@ -5,4 +5,4 @@
 [submodule "coq-serapi"]
 	path = coq-serapi
 	url = https://github.com/ejgallego/coq-serapi.git
-	branch = v8.14
+	branch = v8.15

coq-js/icoq.ml

@@ -105,7 +105,7 @@ let coq_init opts =
   (* Core Coq initialization *)
   Lib.init();
 
-  Global.set_engagement Declarations.PredicativeSet;
+  Global.set_impredicative_set false;
   Global.set_VM false;
   Global.set_native_compiler false;
   Flags.set_native_compiler false;
@@ -138,11 +138,11 @@ let new_doc opts =
 
 let mode_of_stm ~doc sid =
   match Stm.state_of_id ~doc sid with
-  | `Valid (Some { lemmas = Some _; _ }) -> Proof
+  | Valid (Some { lemmas = Some _; _ }) -> Proof
   | _ -> General
 
 let context_of_st m = match m with
-  | `Valid (Some { Vernacstate.lemmas = Some lemma ; _ } ) ->
+  | Stm.Valid (Some { Vernacstate.lemmas = Some lemma ; _ } ) ->
     Vernacstate.LemmaStack.with_top lemma
       ~f:(fun pstate -> Declare.Proof.get_current_context pstate)
   | _ ->
@@ -231,7 +231,7 @@ let compile_vo ~doc vo_out_fn =
   (* freeze and un-freeze to to allow "snapshot" compilation *)
   (*  (normally, save_library_to closes the lib)             *)
   let frz = Vernacstate.freeze_interp_state ~marshallable:false in
-  Library.save_library_to Library.ProofsTodoNone ~output_native_objects:false dirp vo_out_fn (Global.opaque_tables ());
+  Library.save_library_to Library.ProofsTodoNone ~output_native_objects:false dirp vo_out_fn;
   Vernacstate.unfreeze_interp_state frz;
   Js_of_ocaml.Sys_js.read_file ~name:vo_out_fn
 

coq-js/jscoq_doc.ml

@@ -136,14 +136,14 @@ let cancel ~doc can_st =
   in
   let doc, eres = Stm.edit_at ~doc edit_st in
   match eres with
-  | `NewTip -> c_ran, (doc,k_ran)
+  | NewTip -> c_ran, (doc,k_ran)
     (* - [tip] is the new document tip.
        - [st]   -- [stop] is dropped.
        - [stop] -- [tip]  has been kept.
        - [start] is where the editing zone starts
        - [add] happen on top of [id].
     *)
-  | `Focus foc -> cancel_interval edit_st foc, (doc, sdoc)
+  | Focus foc -> cancel_interval edit_st foc, (doc, sdoc)
 
 
 (* Edit is deprecated, we implement it in terms of cancel. *)
@@ -154,8 +154,8 @@ let edit ~doc edit_st =
   else
     let doc, eres = Stm.edit_at ~doc edit_st in
     match eres with
-    | `NewTip    -> let cc, sdoc = split_while sdoc ~f:(fun st -> Stateid.newer_than st edit_st) in cc, (doc, sdoc)
-    | `Focus foc -> cancel_interval edit_st foc, (doc, sdoc)
+    | NewTip    -> let cc, sdoc = split_while sdoc ~f:(fun st -> Stateid.newer_than st edit_st) in cc, (doc, sdoc)
+    | Focus foc -> cancel_interval edit_st foc, (doc, sdoc)
 
 let observe ~doc sid =
   let doc, sdoc = doc in

coq-js/jscoq_doc.mli

@@ -24,7 +24,7 @@ val add :
   ontop:Stateid.t    ->
   newid:Stateid.t    ->
   string             ->
-  Loc.t option * [ `NewTip | `Unfocus of Stateid.t ] * ser_doc
+  Loc.t option * Stm.add_focus * ser_doc
 
 val query :
   doc:ser_doc              ->

coq-serapi @ 9204d486

-Subproject commit 90649c9d1d1ded649cc37d020dc2e41143eea394
+Subproject commit 9204d486b50ed3c6ec5952cdcc895f762378d11c