diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml
index 0b340d1d..c7c3bfa5 100644
--- a/serapi/serapi_protocol.ml
+++ b/serapi/serapi_protocol.ml
@@ -36,7 +36,7 @@ module Extra = struct
 
   (* Custom tokenizer *)
   let rec stream_tok n_tok acc lstr =
-    let e = Gramlib.LStream.next (Pcoq.get_keyword_state()) lstr in
+    let e = Gramlib.LStream.next (Procq.get_keyword_state()) lstr in
     let loc = Gramlib.LStream.get_loc n_tok lstr in
     let l_tok = CAst.make ~loc e in
     if Tok.(equal e EOI) then
@@ -541,7 +541,7 @@ module QueryUtil = struct
   (* This should be moved Coq upstream *)
   let _comments = ref []
   let add_comments pa =
-    let comments = Pcoq.Parsable.comments pa |> List.rev in
+    let comments = Procq.Parsable.comments pa |> List.rev in
     _comments := comments :: !_comments
 
   let libobjects () =
@@ -584,7 +584,7 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object
   | TypeOf id      -> snd (QueryUtil.info_of_id env id)
   | Search         -> [CoqString "Not Implemented"]
   (* XXX: should set printing options in all queries *)
-  | Vernac q       -> let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string q) in
+  | Vernac q       -> let pa = Procq.Parsable.make (Gramlib.Stream.of_string q) in
                       Stm.query ~doc ~at:opt.sid ~route:opt.route pa; []
   (* XXX: Should set the proper sid state *)
   | Env            -> [CoqEnv env]
@@ -699,14 +699,14 @@ module ControlUtil = struct
     let ontop = Extra.value ontop ~default:(Stm.get_current_state ~doc) in
     parsing_state_of_st (Stm.state_of_id ~doc ontop)
     |> Option.map (fun pstate ->
-        let entry = Pcoq.Constr.lconstr in
-        let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string str) in
-        Pcoq.unfreeze pstate;
-        Pcoq.Entry.parse entry pa)
+        let entry = Procq.Constr.lconstr in
+        let pa = Procq.Parsable.make (Gramlib.Stream.of_string str) in
+        Procq.unfreeze pstate;
+        Procq.Entry.parse entry pa)
 
   let parse_sentence ~doc ~ontop sent =
     let ontop = Extra.value ontop ~default:(Stm.get_current_state ~doc) in
-    let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string sent) in
+    let pa = Procq.Parsable.make (Gramlib.Stream.of_string sent) in
     let entry = Pvernac.main_entry in
     Stm.parse_sentence ~doc ontop ~entry pa
 
@@ -719,7 +719,7 @@ module ControlUtil = struct
   exception End_of_input
 
   let add_sentences ~doc opts sent =
-    let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string sent) in
+    let pa = Procq.Parsable.make (Gramlib.Stream.of_string sent) in
     let i   = ref 1                    in
     let acc = ref []                   in
     let stt = ref (Extra.value opts.ontop ~default:(Stm.get_current_state ~doc)) in
diff --git a/sertop/sercomp.ml b/sertop/sercomp.ml
index cfdf8bae..12e5a128 100644
--- a/sertop/sercomp.ml
+++ b/sertop/sercomp.ml
@@ -25,7 +25,7 @@ let input_doc ~input ~in_file ~in_chan ~process ~doc ~sid =
   | I_vernac ->
      begin
        let in_strm = Gramlib.Stream.of_channel in_chan in
-       let in_pa   = Pcoq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file} )) in_strm in
+       let in_pa   = Procq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file} )) in_strm in
        try while true do
            let doc, sid = !stt in
            let east =
diff --git a/sertop/sername.ml b/sertop/sername.ml
index efd38336..3bc54cb7 100644
--- a/sertop/sername.ml
+++ b/sertop/sername.ml
@@ -75,7 +75,7 @@ let sername_doc = "sername Coq tool"
 let do_require ~doc ~sid ~require_lib ~in_file =
   let sent = Printf.sprintf "Require %s." require_lib in
   let in_strm = Gramlib.Stream.of_string sent in
-  let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file})) in_strm in
+  let in_pa = Procq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file})) in_strm in
   match Stm.parse_sentence ~doc ~entry:Pvernac.main_entry sid in_pa with
   | Some ast ->
     let doc, sid, tip = Stm.add ~doc ~ontop:sid false ast in
diff --git a/sertop/sertok.ml b/sertop/sertok.ml
index 1eb08a75..f6dd3cda 100644
--- a/sertop/sertok.ml
+++ b/sertop/sertok.ml
@@ -25,7 +25,7 @@ let load_file f =
   (s)
 
 let rec stream_tok n_tok acc str source begin_line begin_char =
-  let e = Gramlib.LStream.next (Pcoq.get_keyword_state()) str in
+  let e = Gramlib.LStream.next (Procq.get_keyword_state()) str in
   let pre_loc : Loc.t = Gramlib.LStream.get_loc n_tok str in
   let loc =
     { pre_loc with
@@ -48,7 +48,7 @@ let input_doc ~pp ~in_file ~in_chan ~doc ~sid =
   let stt = ref (doc, sid) in
   let in_strm = Gramlib.Stream.of_channel in_chan in
   let source = Loc.InFile { dirpath = None; file = in_file } in
-  let in_pa   = Pcoq.Parsable.make ~loc:(Loc.initial source) in_strm in
+  let in_pa   = Procq.Parsable.make ~loc:(Loc.initial source) in_strm in
   let in_bytes = load_file in_file in
   try while true do
       let l_pre_st = CLexer.Lexer.State.get () in