Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.

1 files changed, 13 insertions, 0 deletions

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index d980b1995f..51b06580e8 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -60,6 +60,19 @@ val set_extern_reference :
 val get_extern_reference :
   unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
 
+(** WARNING: The following functions are evil due to
+    side-effects. Think of the following case as used in the printer:
+
+    without_specific_symbols [SynDefRule kn] (pr_glob_constr_env env) c
+
+    vs
+
+    without_specific_symbols [SynDefRule kn] pr_glob_constr_env env c
+
+    which one is wrong? We should turn this kind of state into an
+    explicit argument.
+*)
+
 (** This forces printing universe names of Type\{.\} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b