diff --git a/coq/parsing.ml b/coq/parsing.ml
index 06737aa4..cddd0d60 100644
--- a/coq/parsing.ml
+++ b/coq/parsing.ml
@@ -1,3 +1,4 @@
+module Pcoq = Procq
 module Parsable = Pcoq.Parsable
 
 let parse ~st ps =
diff --git a/coq/state.mli b/coq/state.mli
index 37dc3d4a..8ea1f911 100644
--- a/coq/state.mli
+++ b/coq/state.mli
@@ -4,7 +4,7 @@ val compare : t -> t -> int
 val equal : t -> t -> bool
 val hash : t -> int
 val mode : st:t -> Pvernac.proof_mode option
-val parsing : st:t -> Pcoq.frozen_t
+val parsing : st:t -> Procq.frozen_t
 
 (** Proof states *)
 module Proof : sig
diff --git a/vendor/coq b/vendor/coq
index 4fc68f45..1ddf4431 160000
--- a/vendor/coq
+++ b/vendor/coq
@@ -1 +1 @@
-Subproject commit 4fc68f4582af6b9e66600925bb09f34eff4012a1
+Subproject commit 1ddf4431751cfdb3c6a96ddb1d53686a2839d3a6