From 04e6672d2f90c7d40d6f9fe7f8c87ab0c063cc02 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 May 2024 19:13:04 +0200 Subject: [PATCH] [build] Fix use of plugin aliases in findlib loading. Newer Coq will raise a warning here, as the acc_tactics build setup is `-warn-on-error` we do fix this now, backwards compatible. --- theories/AAC.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/AAC.v b/theories/AAC.v index 7298663..d1cc3a2 100644 --- a/theories/AAC.v +++ b/theories/AAC.v @@ -960,4 +960,4 @@ Section t. End t. -Declare ML Module "aac_plugin:coq-aac-tactics.plugin". +Declare ML Module "coq-aac-tactics.plugin".