From 9d0fde51068c1f1c16142865457a43d2fd5143ee Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 8 Mar 2013 13:55:12 +0000
Subject: Use with_state_protection in pr_module_vardecls

This makes pr_module_vardecls side effect free, as any pp function should be

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16261 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/ppvernac.ml | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d2f5beedfd..4a91e12849 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -257,15 +257,16 @@ let pr_require_token = function
 let pr_module_vardecls pr_c (export,idl,(mty,inl)) =
   let m = pr_module_ast pr_c mty in
   (* Update the Nametab for interpreting the body of module/modtype *)
-  let lib_dir = Lib.library_dp() in
-  List.iter (fun (_,id) ->
-    Declaremods.process_module_bindings [id]
-      [MBId.make lib_dir id,
-       (Modintern.interp_modtype (Global.env()) mty, inl)]) idl;
-  (* Builds the stream *)
-  spc() ++
-  hov 1 (str"(" ++ pr_require_token export ++
-   prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
+  States.with_state_protection (fun () ->
+    let lib_dir = Lib.library_dp() in
+    List.iter (fun (_,id) ->
+      Declaremods.process_module_bindings [id]
+        [MBId.make lib_dir id,
+         (Modintern.interp_modtype (Global.env()) mty, inl)]) idl;
+    (* Builds the stream *)
+    spc() ++
+    hov 1 (str"(" ++ pr_require_token export ++
+     prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")) ()
 
 let pr_module_binders l pr_c =
   (* Effet de bord complexe pour garantir la declaration des noms des
-- 
cgit v1.2.3