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

7 files changed, 71 insertions, 60 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 9e63df51d..51dd5cd4f 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 2178a7caa..3a8e8fb43 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 d15a811ba..839064aa0 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 5b91f9e68..8945ebadb 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 7b8a38d5f..a025bfff8 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 6972edd52..1b1304db5 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 c00b107cf..10c139e5a 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