[coq] Overlay for coq/coq#18385

SkySkimmer · Jul 8, 2024 · 7bd4cfa · 7bd4cfa
1 parent 04fe925
commit 7bd4cfa
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/theories/Ltac1/Record.v b/theories/Ltac1/Record.v
@@ -2,12 +2,12 @@
 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".
-Declare ML Module "tactician_ltac1_record_plugin:coq-tactician.record-plugin".
+Declare ML Module "coq-core.plugins.ltac".
+Declare ML Module "coq-core.plugins.firstorder_core".
+Declare ML Module "coq-core.plugins.firstorder".
+Declare ML Module "coq-core.plugins.extraction".
+Declare ML Module "coq-core.plugins.funind".
+Declare ML Module "coq-tactician.record-plugin".
 #[export] Set Default Proof Mode "Tactician Ltac1".
 
 Tactician Record Then Decompose.

diff --git a/theories/Ltac1/Tactics.v b/theories/Ltac1/Tactics.v
@@ -1,6 +1,6 @@
 From Tactician Require Export Ltac1.Record.
 
-Declare ML Module "tactician_ltac1_tactics_plugin:coq-tactician.tactics-plugin".
+Declare ML Module "coq-tactician.tactics-plugin".
 
 Tactic Notation (at level 5) "search" "with" "cache" tactic3(t) := fail
   "'search with cache' has been renamed to 'synth with cache'".