Adapt to coq/coq#19690 (Hint Extern follows proof mode)

SkySkimmer · SkySkimmer · commit d2fb128758f1 · 2025-03-12T14:09:45.000+01:00
diff --git a/rupicola b/rupicola
@@ -1 +1 @@
-Subproject commit 78582211b3d9371e3fa03c10ea501820da4ea921
+Subproject commit cae8ce966b6e26536b6c0515ae358feb91d553b7
diff --git a/src/Language/APINotations.v b/src/Language/APINotations.v
@@ -451,6 +451,7 @@ Module Compilers.
   Ltac Reify_rhs _ :=
     ltac2:(_Reify_rhs ()).
 
+  Local Set Default Proof Mode "Classic".
   Global Hint Extern 1 (@expr.Reified_of _ _ _ _ ?t ?v ?rv)
   => cbv [expr.Reified_of]; Reify_rhs (); reflexivity : typeclass_instances.
 
