Merge 8.17 into main (impermeable#61)

Main change according to (PR impermeable#58): we only declare one plugin now.
andres-erbsen · May 18, 2024 · 6de7be1 · 6de7be1
1 parent d43e1c4
commit 6de7be1
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git 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
+END
diff --git 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".
+Declare ML Module "waterproof:coq-waterproof.plugin".
diff --git a/theories/Waterproof.v b/theories/Waterproof.v
@@ -17,4 +17,4 @@
 (******************************************************************************)
 
 From Ltac2 Require Import Init.
-Declare ML Module "waterproof:coq-waterproof.plugin".
+Declare ML Module "waterproof:coq-waterproof.plugin".