From 3fdf345896fedc19f7010fdcdec569d2528ea610 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 May 2024 19:07:44 +0200 Subject: [PATCH] [build] Fix use of plugin aliases in findlib loading. Note that both lines where loading the same plugin, but activating different syntax rules; that's not really allowed as it leaves the system in a partial state. If something like that is needed, true two plugins are necessary (Which is not hard to support nowadays). --- src/databases.mlg | 4 ++-- theories/Automation/Framework.v | 2 +- theories/Waterproof.v | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/databases.mlg b/src/databases.mlg index 8219e95e..2b94763d 100644 --- a/src/databases.mlg +++ b/src/databases.mlg @@ -16,7 +16,7 @@ (* *) (******************************************************************************) -DECLARE PLUGIN "coq-waterproof.databases" +DECLARE PLUGIN "coq-waterproof.plugin" { @@ -73,4 +73,4 @@ VERNAC COMMAND EXTEND DatabaseQuery CLASSIFIED AS QUERY Feedback.msg_notice ((str "Decidability databases :") ++ List.fold_left (fun acc database_name -> acc ++ str " " ++ str database_name) (str "") (get_current_databases Decidability)); Feedback.msg_notice ((str "Shorten databases :") ++ List.fold_left (fun acc database_name -> acc ++ str " " ++ str database_name) (str "") (get_current_databases Shorten)) } -END \ No newline at end of file +END diff --git a/theories/Automation/Framework.v b/theories/Automation/Framework.v index d7b2c0b6..3846d12f 100644 --- a/theories/Automation/Framework.v +++ b/theories/Automation/Framework.v @@ -17,4 +17,4 @@ (******************************************************************************) From Ltac2 Require Import Init. -Declare ML Module "waterproof:coq-waterproof.databases". \ No newline at end of file +Declare ML Module "coq-waterproof.plugin". diff --git a/theories/Waterproof.v b/theories/Waterproof.v index 644e59ae..3846d12f 100644 --- a/theories/Waterproof.v +++ b/theories/Waterproof.v @@ -17,4 +17,4 @@ (******************************************************************************) From Ltac2 Require Import Init. -Declare ML Module "waterproof:coq-waterproof.plugin". \ No newline at end of file +Declare ML Module "coq-waterproof.plugin".