Merge branch 'coq8.11' into coq8.17

coq-tactician · Oct 18, 2023 · 540757f · 540757f
2 parents 116fc19 + e35463b
commit 540757f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Ltac1Dummy.v b/theories/Ltac1Dummy.v
@@ -15,7 +15,7 @@ Tactic Notation (at level 4) "synth" "with" "cache" tactic3(t) := solve [t] || (
   "Check https://coq-tactician.github.io for instructions").
 
 Tactic Notation (at level 4) "synth" := fail
-  "Tactic 'search' requires the Tactician plugin to be installed."
+  "Tactic 'synth' requires the Tactician plugin to be installed."
   "Check https://coq-tactician.github.io for instructions".
 
 Tactic Notation (at level 4) "tactician" "ignore" tactic3(t) := t.