aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrvernac.ml42
1 files changed, 1 insertions, 1 deletions
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