From 27d453641446b3d35aa2211b94f949b57a88ebb2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 1 Mar 2019 15:27:05 +0100
Subject: Stop accessing proof env via Pfedit in printers

This should make https://github.com/coq/coq/pull/9129 easier.
---
 plugins/syntax/g_string.mlg | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/syntax/g_string.mlg')

diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
index 1e06cd8ddb..171e0e213d 100644
--- a/plugins/syntax/g_string.mlg
+++ b/plugins/syntax/g_string.mlg
@@ -21,5 +21,6 @@ open Stdarg
 VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
   | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) ] ->
-    { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
+    { let (sigma, env) = Pfedit.get_current_context () in
+      vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
 END
-- 
cgit v1.2.3