From 7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Sep 2014 18:34:04 +0200 Subject: Removing the XML plugin. Left a README, just in case someone will discover the remnants of it decades from now. --- theories/Init/Prelude.v | 1 - 1 file changed, 1 deletion(-) (limited to 'theories/Init/Prelude.v') diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 01383365e..5d88fa5b7 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -22,6 +22,5 @@ Declare ML Module "decl_mode_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". Declare ML Module "recdef_plugin". -Declare ML Module "xml_plugin". (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_admitted" "_subproof" "Private_". -- cgit v1.2.3