Adapt w.r.t. coq/coq#19313.

ppedrot · Jul 4, 2024 · 0eb39ec · 0eb39ec
1 parent 1b3390a
commit 0eb39ec
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/theories/Ltac1/Record.v b/theories/Ltac1/Record.v
@@ -3,6 +3,7 @@ Definition private_constant_placeholder (x : Type) := x.
 Register private_constant_placeholder as tactician.private_constant_placeholder.
 
 Declare ML Module "ltac_plugin:coq-core.plugins.ltac".
+Declare ML Module "firstorder_core_plugin:coq-core.plugins.firstorder_core".
 Declare ML Module "firstorder_plugin:coq-core.plugins.firstorder".
 Declare ML Module "extraction_plugin:coq-core.plugins.extraction".
 Declare ML Module "funind_plugin:coq-core.plugins.funind".