From 994fb327f05a80f9e951c08ce8c8ac3832566d13 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 May 2024 23:19:30 +0200 Subject: [PATCH] [coq] Overlay for coq/coq#18385 --- theories/Basics/Settings.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Basics/Settings.v b/theories/Basics/Settings.v index cb5d6d4674..d81885f784 100644 --- a/theories/Basics/Settings.v +++ b/theories/Basics/Settings.v @@ -7,9 +7,9 @@ (** ** Plugins *) (** Load the Ltac plugin. This is the tactic language we use for proofs. *) -Declare ML Module "ltac_plugin". +Declare ML Module "ltac_plugin:coq-core.plugins.ltac". (** Load the number string notation plugin. Allowing us to write numbers like [1234]. *) -Declare ML Module "number_string_notation_plugin". +Declare ML Module "number_string_notation_plugin:coq-core.plugins.number_string_notation". (** ** Proofs *)