From d3ea41a30c897791321de503fcb3eed5e079420a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 21 Oct 2024 17:36:56 +0200
Subject: [PATCH] [coq] Adapt to coq/coq#19736

---
 coq/parsing.ml | 1 +
 coq/state.mli  | 2 +-
 vendor/coq     | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

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