[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.

7 files changed, 71 insertions, 60 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 9e63df51de..51dd5cd4f5 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -377,6 +377,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
   Proofview.Goal.enter begin fun gl ->
     let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
     let sigma = Tacmach.New.project gl in
+    let env = Tacmach.New.pf_env gl in
     let u,v = destruct_ind sigma type_of_pq
     in let lb_type_of_p =
         try
@@ -389,7 +390,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
 	    (str "Leibniz->boolean:" ++
              str "You have to declare the" ++
 	     str "decidability over " ++
-	     Printer.pr_econstr type_of_pq ++
+             Printer.pr_econstr_env env sigma type_of_pq ++
 	     str " first.")
           in
           Tacticals.New.tclZEROMSG err_msg
@@ -442,6 +443,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         Proofview.Goal.enter begin fun gl ->
         let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         let sigma = Tacmach.New.project gl in
+        let env = Tacmach.New.pf_env gl in
         if EConstr.eq_constr sigma t1 t2 then aux q1 q2
         else (
           let u,v = try  destruct_ind sigma tt1
@@ -461,7 +463,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
 	                                (str "boolean->Leibniz:" ++
                                          str "You have to declare the" ++
 			   	         str "decidability over " ++
-				         Printer.pr_econstr tt1 ++
+                                         Printer.pr_econstr_env env sigma tt1 ++
 				         str " first.")
 		 in
 		 user_err err_msg
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 2178a7caa0..3a8e8fb436 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -76,7 +76,8 @@ let process_vernac_interp_error exn = match fst exn with
   | Tacred.ReductionTacticError e ->
       wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e ->
-      wrap_vernac_error exn (Himsg.explain_refiner_error e)
+    let sigma, env = Pfedit.get_current_context () in
+    wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e)
   | Nametab.GlobalizationError q ->
       wrap_vernac_error exn
         (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index d15a811ba1..839064aa06 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -92,9 +92,7 @@ let jv_nf_betaiotaevar sigma jl =
 
 (** Printers *)
 
-let pr_lconstr c = quote (pr_lconstr c)
 let pr_lconstr_env e s c = quote (pr_lconstr_env e s c)
-let pr_leconstr c = quote (pr_leconstr c)
 let pr_leconstr_env e s c = quote (pr_leconstr_env e s c)
 let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t)
 
@@ -1037,52 +1035,52 @@ let explain_typeclass_error env = function
 
 (* Refiner errors *)
 
-let explain_refiner_bad_type arg ty conclty =
+let explain_refiner_bad_type env sigma arg ty conclty =
   str "Refiner was given an argument" ++ brk(1,1) ++
-  pr_lconstr arg ++ spc () ++
-  str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++
-  str "instead of" ++ brk(1,1) ++ pr_lconstr conclty ++ str "."
+  pr_lconstr_env env sigma arg ++ spc () ++
+  str "of type" ++ brk(1,1) ++ pr_lconstr_env env sigma ty ++ spc () ++
+  str "instead of" ++ brk(1,1) ++ pr_lconstr_env env sigma conclty ++ str "."
 
 let explain_refiner_unresolved_bindings l =
   str "Unable to find an instance for the " ++
   str (String.plural (List.length l) "variable") ++ spc () ++
   prlist_with_sep pr_comma Name.print l ++ str"."
 
-let explain_refiner_cannot_apply t harg =
+let explain_refiner_cannot_apply env sigma t harg =
   str "In refiner, a term of type" ++ brk(1,1) ++
-  pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
-  pr_lconstr harg ++ str "."
+  pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
+  pr_lconstr_env env sigma harg ++ str "."
 
-let explain_refiner_not_well_typed c =
-  str "The term " ++ pr_lconstr c ++ str " is not well-typed."
+let explain_refiner_not_well_typed env sigma c =
+  str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed."
 
 let explain_intro_needs_product () =
   str "Introduction tactics needs products."
 
-let explain_does_not_occur_in c hyp =
-  str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++
+let explain_does_not_occur_in env sigma c hyp =
+  str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++
   str "does not occur in" ++ spc () ++ Id.print hyp ++ str "."
 
-let explain_non_linear_proof c =
-  str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
+let explain_non_linear_proof env sigma c =
+  str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++
   spc () ++ str "because a metavariable has several occurrences."
 
-let explain_meta_in_type c =
-  str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr c ++
+let explain_meta_in_type env sigma c =
+  str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr_env env sigma c ++
   str " of another meta"
 
 let explain_no_such_hyp id =
   str "No such hypothesis: " ++ Id.print id
 
-let explain_refiner_error = function
-  | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
+let explain_refiner_error env sigma = function
+  | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty
   | UnresolvedBindings t -> explain_refiner_unresolved_bindings t
-  | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg
-  | NotWellTyped c -> explain_refiner_not_well_typed c
+  | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg
+  | NotWellTyped c -> explain_refiner_not_well_typed env sigma c
   | IntroNeedsProduct -> explain_intro_needs_product ()
-  | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp
-  | NonLinearProof c -> explain_non_linear_proof c
-  | MetaInType c -> explain_meta_in_type c
+  | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp
+  | NonLinearProof c -> explain_non_linear_proof env sigma c
+  | MetaInType c -> explain_meta_in_type env sigma c
   | NoSuchHyp id -> explain_no_such_hyp id
 
 (* Inductive errors *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 5b91f9e682..8945ebadb8 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -27,7 +27,7 @@ val explain_typeclass_error : env -> typeclass_error -> Pp.t
 
 val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t
 
-val explain_refiner_error : refiner_error -> Pp.t
+val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t
 
 val explain_pattern_matching_error :
   env -> Evd.evar_map -> pattern_matching_error -> Pp.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7b8a38d5f6..a025bfff83 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -253,7 +253,9 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
         | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
         | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
         | App (t, args) -> mkApp (body_i t, args)
-        | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body ++ str ".") in
+        | _ ->
+          let sigma, env = Pfedit.get_current_context () in
+          anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in
       let body_i = body_i body in
       match locality with
       | Discharge ->
@@ -530,7 +532,5 @@ let save_proof ?proof = function
       Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
 
 (* Miscellaneous *)
+let get_current_context () = Pfedit.get_current_context ()
 
-let get_current_context () =
-  Pfedit.get_current_context ()
-           
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 6972edd52f..1b1304db5b 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -66,3 +66,4 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
+[@@ocaml.deprecated "please use [Pfedit.get_current_context]"]
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c00b107cfe..10c139e5ab 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -56,8 +56,9 @@ let scope_class_of_qualid qid =
 let show_proof () =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   let p = Proof_global.give_me_the_proof () in
+  let sigma, env = Pfedit.get_current_context () in
   let pprf = Proof.partial_proof p in
-  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf)
+  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
 
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
@@ -255,7 +256,8 @@ let print_namespace ns =
   let print_constant k body =
     (* FIXME: universes *)
     let t = body.Declarations.const_type in
-    print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
+    let sigma, env = Pfedit.get_current_context () in
+    print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t
   in
   let matches mp = match match_modulepath ns mp with
   | Some [] -> true
@@ -484,8 +486,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
  	let red_option = match red_option with
           | None -> None
           | Some r ->
-	      let (evc,env)= get_current_context () in
- 		Some (snd (Hook.get f_interp_redexp env evc r)) in
+            let sigma, env= Pfedit.get_current_context () in
+            Some (snd (Hook.get f_interp_redexp env sigma r)) in
 	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof locality p kind l =
@@ -1537,7 +1539,7 @@ let vernac_print_option key =
 
 let get_current_context_of_args = function
   | Some n -> Pfedit.get_goal_context n
-  | None -> get_current_context ()
+  | None -> Pfedit.get_current_context ()
 
 let query_command_selector ?loc = function
   | None -> None
@@ -1626,17 +1628,20 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt =
     let natureofid = match decl with
                      | LocalAssum _ -> "Hypothesis"
                      | LocalDef (_,bdy,_) ->"Constant (let in)" in
-    v 0 (Id.print id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
+    let sigma, env = Pfedit.get_current_context () in
+    v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl()
 	 ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
-    | NoHyp | Not_found -> print_about ref_or_by_not
+    | NoHyp | Not_found ->
+    let sigma, env = Pfedit.get_current_context () in
+    print_about env sigma ref_or_by_not
 
-	       
-let vernac_print ?loc = let open Feedback in function
+
+let vernac_print ?loc env sigma = let open Feedback in function
   | PrintTables -> msg_notice (print_tables ())
-  | PrintFullContext-> msg_notice (print_full_context_typ ())
-  | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
-  | PrintInspect n -> msg_notice (inspect n)
+  | PrintFullContext-> msg_notice (print_full_context_typ env sigma)
+  | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid)
+  | PrintInspect n -> msg_notice (inspect env sigma n)
   | PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent)
   | PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir)
   | PrintModules -> msg_notice (print_modules ())
@@ -1646,15 +1651,15 @@ let vernac_print ?loc = let open Feedback in function
   | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
   | PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
   | PrintDebugGC -> msg_notice (Mltop.print_gc ())
-  | PrintName qid -> dump_global qid; msg_notice (print_name qid)
+  | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid)
   | PrintGraph -> msg_notice (Prettyp.print_graph())
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
   | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
-  | PrintCoercions -> msg_notice (Prettyp.print_coercions())
+  | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma)
   | PrintCoercionPaths (cls,clt) ->
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
-  | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
+  | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma)
   | PrintUniverses (b, dst) ->
      let univ = Global.universes () in
      let univ = if b then UGraph.sort_universes univ else univ in
@@ -1666,16 +1671,16 @@ let vernac_print ?loc = let open Feedback in function
      | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
      | Some s -> dump_universes_gen univ s
      end
-  | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
+  | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r))
   | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
-  | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s)
-  | PrintHintDb -> msg_notice (Hints.pr_searchtable ())
+  | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s)
+  | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma)
   | PrintScopes ->
-      msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
+      msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)))
   | PrintScope s ->
-      msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
+      msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
   | PrintVisibility s ->
-      msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
+      msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
   | PrintAbout (ref_or_by_not,glnumopt) ->
      msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt)
   | PrintImplicit qid ->
@@ -1778,9 +1783,10 @@ let vernac_locate = let open Feedback in function
   | LocateTerm (AN qid) -> msg_notice (print_located_term qid)
   | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *)
   | LocateTerm (ByNotation (_, (ntn, sc))) ->
-      msg_notice
-        (Notation.locate_notation
-          (Constrextern.without_symbols pr_lglob_constr) ntn sc)
+    let _, env = Pfedit.get_current_context () in
+    msg_notice
+      (Notation.locate_notation
+         (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc)
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> msg_notice (print_located_module qid)
   | LocateOther (s, qid) -> msg_notice (print_located_other s qid)
@@ -1847,10 +1853,11 @@ let vernac_bullet (bullet : Proof_bullet.t) =
 let vernac_show = let open Feedback in function
   | ShowScript -> assert false  (* Only the stm knows the script *)
   | ShowGoal goalref ->
+    let proof = Proof_global.give_me_the_proof () in
     let info = match goalref with
-      | OpenSubgoals -> pr_open_subgoals ()
-      | NthGoal n -> pr_nth_open_subgoal n
-      | GoalId id -> pr_goal_by_id id
+      | OpenSubgoals -> pr_open_subgoals ~proof
+      | NthGoal n -> pr_nth_open_subgoal ~proof n
+      | GoalId id -> pr_goal_by_id ~proof id
     in
     msg_notice info
   | ShowProof -> show_proof ()
@@ -2041,7 +2048,9 @@ let interp ?proof ?loc locality poly st c =
   | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ?loc r g c
   | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
   | VernacGlobalCheck c -> vernac_global_check c
-  | VernacPrint p -> vernac_print ?loc p
+  | VernacPrint p ->
+    let sigma, env = Pfedit.get_current_context () in
+    vernac_print ?loc env sigma p
   | VernacSearch (s,g,r) -> vernac_search ?loc s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r