From 25b07a6f824654be2041152d904507bc62102986 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 28 Feb 2018 13:45:04 +0100 Subject: Implement the Export Set/Unset feature. This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313. --- plugins/ssr/ssrvernac.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index e3941c1c5..c3b6a7c59 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -178,7 +178,7 @@ GEXTEND Gram GLOBAL: gallina_ext; gallina_ext: [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" -> - Vernacexpr.VernacUnsetOption (["Printing"; "Implicit"; "Defensive"]) + Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) ] ] ; END -- cgit v1.2.3