From 1c9562e12d22b2c72118accc9222a428707df537 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 15 Oct 2024 11:39:09 +0200
Subject: [PATCH] Adapt to coq/coq#19690 (Hint Extern respects default proof
 mode)

---
 src/Rupicola/Lib/IdentParsing.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Rupicola/Lib/IdentParsing.v b/src/Rupicola/Lib/IdentParsing.v
index dbb54e71..f1b723c9 100644
--- a/src/Rupicola/Lib/IdentParsing.v
+++ b/src/Rupicola/Lib/IdentParsing.v
@@ -326,6 +326,8 @@ Module TC.
            end).
 
   Class __IdentToString := __identToString: string.
+
+  Set Default Proof Mode "Classic". (* after Rocq 9, Default Proof Mode "Ltac2" will parse hint extern as ltac2 *)
   #[global] Hint Extern 1 __IdentToString => serialize_ident_in_context : typeclass_instances.
 
   Notation ident_to_string a :=