[printing] Deprecate all printing functions accessing the global proof.

We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.

We also adapt most of the code, making more explicit where the
printing environment is coming from.

An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.

9 files changed, 69 insertions, 52 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index d0424eb89..fa8435d1f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -388,7 +388,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
 	 Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
        else Tacticals.New.tclFAIL 0 (str"Unbound reference")
        end
-    | Extern tacast -> 
+    | Extern tacast ->
       conclPattern concl p tacast
   in
   let pr_hint () =
@@ -396,7 +396,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
     | None -> mt ()
     | Some n -> str " (in " ++ str n ++ str ")"
     in
-    pr_hint t ++ origin
+    let sigma, env = Pfedit.get_current_context () in
+    pr_hint env sigma t ++ origin
   in
   tclLOG dbg pr_hint (run_hint t tactic)
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e68087f14..6a9cd7e20 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -74,12 +74,12 @@ let find_matches bas pat =
   let res = HintDN.search_pattern base pat in
   List.map snd res
 
-let print_rewrite_hintdb bas =
+let print_rewrite_hintdb env sigma bas =
   (str "Database " ++ str bas ++ fnl () ++
 	   prlist_with_sep fnl
 	   (fun h ->
 	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
-	       Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
+               Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++
 	       Option.cata (fun tac -> str " then use tactic " ++
 	       Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
 	   (find_rewrites bas))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index d2b5e070b..44acf3c01 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -40,7 +40,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni
 
 val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
 
-val print_rewrite_hintdb : string -> Pp.t
+val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t
 
 open Clenv
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b98b10315..cee6d4bea 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -464,15 +464,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
       in
       let tac = run_hint t tac in
       let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
+      let _, env = Pfedit.get_current_context () in
       let pp =
         match p with
         | Some pat when get_typeclasses_filtered_unification () ->
-           str " with pattern " ++ Printer.pr_constr_pattern pat
+           str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat
         | _ -> mt ()
       in
         match repr_hint t with
-        | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp))
-        | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp))
+        | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp))
+        | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 239661498..f5c6ab879 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -178,7 +178,8 @@ and e_my_find_search sigma db_list local_db secvars hdc concl =
         | Extern tacast -> conclPattern concl p tacast
        in
        let tac = run_hint t tac in
-       (tac, lazy (pr_hint t)))
+       let sigma, env = Pfedit.get_current_context () in
+       (tac, lazy (pr_hint env sigma t)))
   in
   List.map tac_of_hint hintl
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 99be1846c..70e84013b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1392,14 +1392,14 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_hint_elt (c, _, _) = pr_econstr c
+let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c
 
-let pr_hint h = match h.obj with
-  | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
-  | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c)
-  | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c)
+let pr_hint env sigma h = match h.obj with
+  | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c)
+  | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c)
+  | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c)
   | Res_pf_THEN_trivial_fail (c, _) ->
-      (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial")
+      (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
   | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
   | Extern tac ->
       let env =
@@ -1410,21 +1410,21 @@ let pr_hint h = match h.obj with
       in
       (str "(*external*) " ++ Pputils.pr_glb_generic env tac)
 
-let pr_id_hint (id, v) =
-  let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in
-  (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
+let pr_id_hint env sigma (id, v) =
+  let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in
+  (pr_hint env sigma v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
    ++ str", id " ++ int id ++ str ")" ++ spc ())
 
-let pr_hint_list hintlist =
-  (str "  " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
+let pr_hint_list env sigma hintlist =
+  (str "  " ++ hov 0 (prlist (pr_id_hint env sigma) hintlist) ++ fnl ())
 
-let pr_hints_db (name,db,hintlist) =
+let pr_hints_db env sigma (name,db,hintlist) =
   (str "In the database " ++ str name ++ str ":" ++
      if List.is_empty hintlist then (str " nothing" ++ fnl ())
-     else (fnl () ++ pr_hint_list hintlist))
+     else (fnl () ++ pr_hint_list env sigma hintlist))
 
 (* Print all hints associated to head c in any database *)
-let pr_hint_list_for_head c =
+let pr_hint_list_for_head env sigma c =
   let dbs = current_db () in
   let validate (name, db) =
     let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in
@@ -1436,13 +1436,13 @@ let pr_hint_list_for_head c =
   else
     hov 0
       (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++
-	 hov 0 (prlist pr_hints_db valid_dbs))
+         hov 0 (prlist (pr_hints_db env sigma) valid_dbs))
 
 let pr_hint_ref ref = pr_hint_list_for_head ref
 
 (* Print all hints associated to head id in any database *)
 
-let pr_hint_term sigma cl =
+let pr_hint_term env sigma cl =
   try
     let dbs = current_db () in
     let valid_dbs =
@@ -1460,18 +1460,19 @@ let pr_hint_term sigma cl =
 	(str "No hint applicable for current goal")
       else
 	(str "Applicable Hints :" ++ fnl () ++
-	    hov 0 (prlist pr_hints_db valid_dbs))
+            hov 0 (prlist (pr_hints_db env sigma) valid_dbs))
   with Match_failure _ | Failure _ ->
     (str "No hint applicable for current goal")
 
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint () =
+  let env = Global.env () in
   let pts = Proof_global.give_me_the_proof () in
   let glss,_,_,_,sigma = Proof.proof pts in
   match glss with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
   | g::_ ->
-    pr_hint_term sigma (Goal.V82.concl sigma g)
+    pr_hint_term env sigma (Goal.V82.concl sigma g)
 
 let pp_hint_mode = function
   | ModeInput -> str"+"
@@ -1479,9 +1480,9 @@ let pp_hint_mode = function
   | ModeOutput -> str"-"
 
 (* displays the whole hint database db *)
-let pr_hint_db db =
+let pr_hint_db_env env sigma db =
   let pr_mode = prvect_with_sep spc pp_hint_mode in
-  let pr_modes l = 
+  let pr_modes l =
     if List.is_empty l then mt ()
     else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")"
   in
@@ -1491,7 +1492,7 @@ let pr_hint_db db =
       | None -> str "For any goal"
       | Some head -> str "For " ++ pr_global head ++ pr_modes modes
       in
-      let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in
+      let hints = pr_hint_list env sigma (List.map (fun x -> (0, x)) hintlist) in
       let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in
       accu ++ hint_descr
     in
@@ -1506,17 +1507,21 @@ let pr_hint_db db =
   hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++
   content
 
-let pr_hint_db_by_name dbname =
+let pr_hint_db db =
+  let sigma, env = Pfedit.get_current_context () in
+  pr_hint_db_env env sigma db
+
+let pr_hint_db_by_name env sigma dbname =
   try
-    let db = searchtable_map dbname in pr_hint_db db
+    let db = searchtable_map dbname in pr_hint_db_env env sigma db
   with Not_found ->
     error_no_such_hint_database dbname
 
 (* displays all the hints of all databases *)
-let pr_searchtable () =
+let pr_searchtable env sigma =
   let fold name db accu =
     accu ++ str "In the database " ++ str name ++ str ":" ++ fnl () ++
-    pr_hint_db db ++ fnl ()
+    pr_hint_db_env env sigma db ++ fnl ()
   in
   Hintdbmap.fold fold !searchtable (mt ())
 
@@ -1534,10 +1539,13 @@ let warn_non_imported_hint =
           strbrk "Hint used but not imported: " ++ hint ++ print_mp mp)
 
 let warn h x =
-  let hint = pr_hint h in
-  let (mp, _, _) = KerName.repr h.uid in
-  warn_non_imported_hint (hint,mp);
-  Proofview.tclUNIT x
+  let open Proofview in
+  tclBIND tclENV     (fun env   ->
+  tclBIND tclEVARMAP (fun sigma ->
+          let hint = pr_hint env sigma h in
+          let (mp, _, _) = KerName.repr h.uid in
+          warn_non_imported_hint (hint,mp);
+          Proofview.tclUNIT x))
 
 let run_hint tac k = match !warn_hint with
 | `LAX -> k tac.obj
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 22df29b80..cbf204981 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -260,14 +260,15 @@ val rewrite_db : hint_db_name
 
 (** Printing  hints *)
 
-val pr_searchtable : unit -> Pp.t
+val pr_searchtable : env -> evar_map -> Pp.t
 val pr_applicable_hint : unit -> Pp.t
-val pr_hint_ref : global_reference -> Pp.t
-val pr_hint_db_by_name : hint_db_name -> Pp.t
+val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t
+val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
+val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
 val pr_hint_db : Hint_db.t -> Pp.t
-val pr_hint : hint -> Pp.t
+[@@ocaml.deprecated "please used pr_hint_db_env"]
+val pr_hint : env -> evar_map -> hint -> Pp.t
 
 (** Hook for changing the initialization of auto *)
-
 val add_hints_init : (unit -> unit) -> unit
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 8648dfb90..46b10bf33 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -282,10 +282,11 @@ let generalizeRewriteIntros as_mode tac depids id =
 let error_too_many_names pats =
   let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in
   Proofview.tclENV >>= fun env ->
+  Proofview.tclEVARMAP >>= fun sigma ->
   tclZEROMSG ?loc (
     str "Unexpected " ++
     str (String.plural (List.length pats) "introduction pattern") ++
-    str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
+    str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
     str ".")
 
 let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 15c25b346..e072bd95f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -945,10 +945,14 @@ let reduction_clause redexp cl =
 	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
 
 let reduce redexp cl =
-  let trace () =
+  let trace env sigma =
     let open Printer in
-    let pr = (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern) in
-    Pp.(hov 2 (Pputils.pr_red_expr pr str redexp))
+    let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in
+    Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp))
+  in
+  let trace () =
+    let sigma, env = Pfedit.get_current_context () in
+    trace env sigma
   in
   Proofview.Trace.name_tactic trace begin
   Proofview.Goal.enter begin fun gl ->
@@ -3128,11 +3132,11 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
 
 let warn_unused_intro_pattern env sigma =
   CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics"
-         (fun names ->
-          strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
-          ++ str": " ++ prlist_with_sep spc 
-         (Miscprint.pr_intro_pattern 
-	 (fun c -> Printer.pr_econstr (snd (c env sigma)))) names)
+    (fun names ->
+       strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++
+       str": " ++ prlist_with_sep spc
+         (Miscprint.pr_intro_pattern
+            (fun c -> Printer.pr_econstr_env env sigma (snd (c env sigma)))) names)
 
 let check_unused_names env sigma names =
   if not (List.is_empty names) then