Stop accessing proof env via Pfedit in printers

This should make https://github.com/coq/coq/pull/9129 easier.

8 files changed, 126 insertions, 113 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 58daa7a7d4..6956120a6a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1232,7 +1232,7 @@ let abs_wgen keep_let f gen (gl,args,c) =
   let evar_closed t p =
     if occur_existential sigma t then
       CErrors.user_err ?loc:(loc_of_cpattern p) ~hdr:"ssreflect"
-        (pr_constr_pat (EConstr.Unsafe.to_constr t) ++
+        (pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++
         str" contains holes and matches no subterm of the goal") in
   match gen with
   | _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) ->
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 82a88678f0..3fc05437da 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -133,7 +133,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   | _ -> false in
   let match_pat env p occ h cl = 
     let sigma0 = project orig_gl in
-    ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern p));
+    ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p));
     let (c,ucst), cl =
       fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in
     ppdebug(lazy Pp.(str"     got: " ++ pr_constr_env env sigma0 c));
@@ -239,8 +239,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
       let elimty = Reductionops.whd_all env (project gl) elimty in
       seed, cty, elim, elimty, elim_args, n_elim_args, elim_is_dep, is_rec, pred, gl
   in
-  ppdebug(lazy Pp.(str"elim= "++ pr_constr_pat (EConstr.Unsafe.to_constr elim)));
-  ppdebug(lazy Pp.(str"elimty= "++ pr_constr_pat (EConstr.Unsafe.to_constr elimty)));
+  ppdebug(lazy Pp.(str"elim= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elim)));
+  ppdebug(lazy Pp.(str"elimty= "++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr elimty)));
   let inf_deps_r = match EConstr.kind_of_type (project gl) elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
     | _ -> assert false in
@@ -285,8 +285,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   (* Patterns for the inductive types indexes to be bound in pred are computed
    * looking at the ones provided by the user and the inferred ones looking at
    * the type of the elimination principle *)
-  let pp_pat (_,p,_,occ) = Pp.(pr_occ occ ++ pp_pattern p) in
-  let pp_inf_pat gl (_,_,t,_) = pr_constr_pat (EConstr.Unsafe.to_constr (fire_subst gl t)) in
+  let pp_pat (_,p,_,occ) = Pp.(pr_occ occ ++ pp_pattern env p) in
+  let pp_inf_pat gl (_,_,t,_) = pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl t)) in
   let patterns, clr, gl =
     let rec loop patterns clr i = function
       | [],[] -> patterns, clr, gl
@@ -300,7 +300,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
           loop (patterns @ [i, p, inf_t, occ]) 
             (clr_t @ clr) (i+1) (deps, inf_deps)
       | [], c :: inf_deps -> 
-          ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_constr_pat (EConstr.Unsafe.to_constr c)));
+          ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr c)));
           loop (patterns @ [i, mkTpat gl c, c, allocc]) 
             clr (i+1) ([], inf_deps)
       | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in
@@ -323,11 +323,11 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
   let elim_pred, gen_eq_tac, clr, gl = 
     let error gl t inf_t = errorstrm Pp.(str"The given pattern matches the term"++
       spc()++pp_term gl t++spc()++str"while the inferred pattern"++
-      spc()++pr_constr_pat (EConstr.Unsafe.to_constr (fire_subst gl inf_t))++spc()++ str"doesn't") in
+      spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl inf_t))++spc()++ str"doesn't") in
     let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) =
       let p = unif_redex gl p inf_t in
       if is_undef_pat p then
-        let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern p)) in
+        let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern env p)) in
         cl, gl, post @ [h, p, inf_t, occ]
       else try
         let c, cl, ucst = match_pat env p occ h cl in
@@ -408,7 +408,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
     if not (Evar.Set.is_empty inter) then begin
       let i = Evar.Set.choose inter in
       let pat = List.find (fun t -> Evar.Set.mem i (evars_of_term t)) patterns in
-      errorstrm Pp.(str"Pattern"++spc()++pr_constr_pat (EConstr.Unsafe.to_constr pat)++spc()++
+      errorstrm Pp.(str"Pattern"++spc()++pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr pat)++spc()++
         str"was not completely instantiated and one of its variables"++spc()++
         str"occurs in the type of another non-instantiated pattern variable");
     end
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 18461c0533..15480c7a45 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -199,13 +199,13 @@ let simplintac occ rdx sim gl =
   | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (donetac n)) gl
   | _ -> simpltac sim gl
 
-let rec get_evalref sigma c = match EConstr.kind sigma c with
+let rec get_evalref env sigma c = match EConstr.kind sigma c with
   | Var id -> EvalVarRef id
   | Const (k,_) -> EvalConstRef k
-  | App (c', _) -> get_evalref sigma c'
-  | Cast (c', _, _) -> get_evalref sigma c'
+  | App (c', _) -> get_evalref env sigma c'
+  | Cast (c', _, _) -> get_evalref env sigma c'
   | Proj(c,_) -> EvalConstRef(Projection.constant c)
-  | _ -> errorstrm Pp.(str "The term " ++ pr_constr_pat (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable")
+  | _ -> errorstrm Pp.(str "The term " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable")
 
 (* Strip a pattern generated by a prenex implicit to its constant. *)
 let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with
@@ -230,7 +230,7 @@ let unfoldintac occ rdx t (kt,_) gl =
   let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
   let (sigma, t), const = strip_unfold_term env0 t kt in
   let body env t c =
-    Tacred.unfoldn [AllOccurrences, get_evalref sigma t] env sigma0 c in
+    Tacred.unfoldn [AllOccurrences, get_evalref env sigma t] env sigma0 c in
   let easy = occ = None && rdx = None in
   let red_flags = if easy then CClosure.betaiotazeta else CClosure.betaiota in
   let beta env = Reductionops.clos_norm_flags red_flags env sigma0 in
@@ -244,7 +244,7 @@ let unfoldintac occ rdx t (kt,_) gl =
       try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c)))
       with NoMatch when easy -> c
       | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of "
-        ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)),
+        ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)),
     (fun () -> try end_T () with 
       | NoMatch when easy -> fake_pmatcher_end () 
       | NoMatch -> anomaly "unfoldintac")
@@ -270,12 +270,12 @@ let unfoldintac occ rdx t (kt,_) gl =
       else
         try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t)
         with _ -> errorstrm Pp.(str "The term " ++
-          pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))),
+          pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t))),
     fake_pmatcher_end in
   let concl = 
     let concl0 = EConstr.Unsafe.to_constr concl0 in
     try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) 
-    with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_constr_pat (EConstr.Unsafe.to_constr t)) in
+    with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_constr_pat env0 sigma (EConstr.Unsafe.to_constr t)) in
   let _ = conclude () in
   Proofview.V82.of_tactic (convert_concl concl) gl
 ;;
@@ -298,8 +298,8 @@ let foldtac occ rdx ft gl =
        try
          let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in
          EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
-    with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat t ++ spc ()
-      ++ str "does not match redex " ++ pr_constr_pat c)), 
+    with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat env sigma t ++ spc ()
+      ++ str "does not match redex " ++ pr_constr_pat env sigma c)),
     fake_pmatcher_end in
   let concl0 = EConstr.Unsafe.to_constr concl0 in
   let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in
@@ -412,7 +412,7 @@ let rwcltac cl rdx dir sr gl =
       let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
       let r3, _, r3t  = 
         try EConstr.destCast (project gl) r2 with _ ->
-        errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr))
+        errorstrm Pp.(str "no cast from " ++ pr_constr_pat (pf_env gl) (project gl) (EConstr.Unsafe.to_constr (snd sr))
                     ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in
       let cl' = EConstr.mkNamedProd (make_annot rule_id Sorts.Relevant) (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
       let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in
@@ -473,7 +473,7 @@ let rwprocess_rule dir rule gl =
       let t =
         if red = 1 then Tacred.hnf_constr env sigma t0
         else Reductionops.whd_betaiotazeta sigma t0 in
-      ppdebug(lazy Pp.(str"rewrule="++pr_constr_pat (EConstr.Unsafe.to_constr t)));
+      ppdebug(lazy Pp.(str"rewrule="++pr_constr_pat env sigma (EConstr.Unsafe.to_constr t)));
       match EConstr.kind sigma t with
       | Prod (_, xt, at) ->
         let sigma = Evd.create_evar_defs sigma in
@@ -532,8 +532,8 @@ let rwprocess_rule dir rule gl =
         sigma, (d, r', lhs, rhs) :: rs
       | _ ->
         if red = 0 then loop d sigma r t rs 1
-        else errorstrm Pp.(str "not a rewritable relation: " ++ pr_constr_pat (EConstr.Unsafe.to_constr t)
-                        ++ spc() ++ str "in rule " ++ pr_constr_pat  (EConstr.Unsafe.to_constr (snd rule)))
+        else errorstrm Pp.(str "not a rewritable relation: " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr t)
+                        ++ spc() ++ str "in rule " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr (snd rule)))
         in
     let sigma, r = rule in
     let t = Retyping.get_type_of env sigma r in
@@ -547,9 +547,9 @@ let rwrxtac occ rdx_pat dir rule gl =
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
-        errorstrm Pp.(str "pattern " ++ pr_constr_pat (EConstr.Unsafe.to_constr rdx) ++
+        errorstrm Pp.(str "pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr rdx) ++
                    str " does not match " ++ pr_dir_side dir ++
-                   str " of " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd rule)))
+                   str " of " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (snd rule)))
       | (d, r, lhs, rhs) :: rs ->
         try
           let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in
@@ -640,7 +640,7 @@ let ssrrewritetac ist rwargs =
 let unfoldtac occ ko t kt gl =
   let env = pf_env gl in
   let cl, c = pf_fill_occ_term gl occ (fst (strip_unfold_term env t kt)) in
-  let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref (project gl) c] gl c) cl in
+  let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in
   let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in
   Proofview.V82.of_tactic
     (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 9ea35b8694..be9586fdd7 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -50,7 +50,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
   let c = EConstr.of_constr c in
   let cl = EConstr.of_constr cl in
   if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++
-    pr_constr_pat (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++
+    pr_constr_pat env sigma (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++
     str"Did you mean pose?") else
   let c, (gl, cty) =  match EConstr.kind sigma c with
   | Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 2a2cd73df2..0ec5f1673a 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -74,11 +74,11 @@ let frozen_lexer = CLexer.get_keyword_state () ;;
 
 let tacltop = (5,Notation_gram.E)
 
-let pr_ssrtacarg _ _ prt = prt tacltop
+let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop
 
 }
 
-ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg }
+ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
 | [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") }
 END
 GRAMMAR EXTEND Gram
@@ -89,12 +89,12 @@ END
 {
 
 (* Lexically closed tactic for tacticals. *)
-let pr_ssrtclarg _ _ prt tac = prt tacltop tac
+let pr_ssrtclarg env sigma _ _ prt tac = prt env sigma tacltop tac
 
 }
 
 ARGUMENT EXTEND ssrtclarg TYPED AS ssrtacarg
-    PRINTED BY { pr_ssrtclarg }
+    PRINTED BY { pr_ssrtclarg env sigma }
 | [ ssrtacarg(tac) ] -> { tac }
 END
 
@@ -109,7 +109,7 @@ let add_genarg tag pr =
   let glob ist x = (ist, x) in
   let subst _ x = x in
   let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in
-  let gen_pr _ _ _ = pr in
+  let gen_pr env sigma _ _ _ = pr env sigma in
   let () = Genintern.register_intern0 wit glob in
   let () = Genintern.register_subst0 wit subst in
   let () = Geninterp.register_interp0 wit interp in
@@ -146,7 +146,7 @@ let pr_list = prlist_with_sep
 
 let pr_ssrhyp _ _ _ = pr_hyp
 
-let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp
+let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp)
 
 let intern_hyp ist (SsrHyp (loc, id) as hyp) =
   let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in
@@ -168,7 +168,7 @@ END
 let pr_hoi = hoik pr_hyp
 let pr_ssrhoi _ _ _ = pr_hoi
 
-let wit_ssrhoirep = add_genarg "ssrhoirep" pr_hoi
+let wit_ssrhoirep = add_genarg "ssrhoirep" (fun env sigma -> pr_hoi)
 
 let intern_ssrhoi ist = function
   | Hyp h -> Hyp (intern_hyp ist h)
@@ -212,13 +212,13 @@ END
 
 let pr_rwdir = function L2R -> mt() | R2L -> str "-"
 
-let wit_ssrdir = add_genarg "ssrdir" pr_dir
+let wit_ssrdir = add_genarg "ssrdir" (fun env sigma -> pr_dir)
 
 (** Simpl switch *)
 
 let pr_ssrsimpl _ _ _ = pr_simpl
 
-let wit_ssrsimplrep = add_genarg "ssrsimplrep" pr_simpl
+let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl)
 
 let test_ssrslashnum b1 b2 strm =
   match Util.stream_nth 0 strm with
@@ -413,7 +413,7 @@ END
 
 let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt ()
 
-let wit_ssrmmod = add_genarg "ssrmmod" pr_mmod
+let wit_ssrmmod = add_genarg "ssrmmod" (fun env sigma -> pr_mmod)
 let ssrmmod = Pcoq.create_generic_entry Pcoq.utactic "ssrmmod" (Genarg.rawwit wit_ssrmmod);;
 
 }
@@ -643,7 +643,7 @@ and map_block map_id = function
   | SuffixNum _ as x -> x
 
 type ssripatrep = ssripat
-let wit_ssripatrep = add_genarg "ssripatrep" pr_ipat
+let wit_ssripatrep = add_genarg "ssripatrep" (fun env sigma -> pr_ipat)
 
 let pr_ssripat _ _ _ = pr_ipat
 let pr_ssripats _ _ _ = pr_ipats
@@ -950,13 +950,13 @@ END
 
 {
 
-let pr_ssrintrosarg _ _ prt (tac, ipats) =
-  prt tacltop tac ++ pr_intros spc ipats
+let pr_ssrintrosarg env sigma _ _ prt (tac, ipats) =
+  prt env sigma tacltop tac ++ pr_intros spc ipats
 
 }
 
 ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros)
-   PRINTED BY { pr_ssrintrosarg }
+   PRINTED BY { pr_ssrintrosarg env sigma }
 | [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats }
 END
 
@@ -1007,22 +1007,22 @@ GRAMMAR EXTEND Gram
 
 {
 
-let pr_ortacs prt = 
+let pr_ortacs env sigma prt =
   let rec pr_rec = function
   | [None]           -> spc() ++ str "|" ++ spc()
   | None :: tacs     -> spc() ++ str "|" ++ pr_rec tacs
-  | Some tac :: tacs -> spc() ++ str "| " ++ prt tacltop tac ++  pr_rec tacs
+  | Some tac :: tacs -> spc() ++ str "| " ++ prt env sigma tacltop tac ++  pr_rec tacs
   | []                -> mt() in
   function
   | [None]           -> spc()
   | None :: tacs     -> pr_rec tacs
-  | Some tac :: tacs -> prt tacltop tac ++ pr_rec tacs
+  | Some tac :: tacs -> prt env sigma tacltop tac ++ pr_rec tacs
   | []                -> mt()
-let pr_ssrortacs _ _ = pr_ortacs
+let pr_ssrortacs env sigma _ _ = pr_ortacs env sigma
 
 }
 
-ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY { pr_ssrortacs }
+ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY { pr_ssrortacs env sigma }
 | [ ssrtacarg(tac) "|" ssrortacs(tacs) ] -> { Some tac :: tacs }
 | [ ssrtacarg(tac) "|" ] -> { [Some tac; None] }
 | [ ssrtacarg(tac) ] -> { [Some tac] }
@@ -1032,34 +1032,34 @@ END
 
 {
 
-let pr_hintarg prt = function
-  | true, tacs -> hv 0 (str "[ " ++ pr_ortacs prt tacs ++ str " ]")
-  | false, [Some tac] -> prt tacltop tac
+let pr_hintarg env sigma prt = function
+  | true, tacs -> hv 0 (str "[ " ++ pr_ortacs env sigma prt tacs ++ str " ]")
+  | false, [Some tac] -> prt env sigma tacltop tac
   | _, _ -> mt()
 
-let pr_ssrhintarg _ _ = pr_hintarg
+let pr_ssrhintarg env sigma _ _ = pr_hintarg env sigma
 
 }
 
-ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg }
+ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma }
 | [ "[" "]" ] -> { nullhint }
 | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
 | [ ssrtacarg(arg) ] -> { mk_hint arg }
 END
 
-ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg }
+ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma }
 | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
 END
 
 {
 
-let pr_hint prt arg =
-  if arg = nohint then mt() else str "by " ++ pr_hintarg prt arg
-let pr_ssrhint _ _ = pr_hint
+let pr_hint env sigma prt arg =
+  if arg = nohint then mt() else str "by " ++ pr_hintarg env sigma prt arg
+let pr_ssrhint env sigma _ _ = pr_hint env sigma
 
 }
 
-ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY { pr_ssrhint }
+ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY { pr_ssrhint env sigma }
 | [ ]                       -> { nohint }
 END
 (** The "in" pseudo-tactical *)
@@ -1117,7 +1117,7 @@ let pr_clseq = function
   | InHypsSeq       -> str " |-"
   | InAllHyps       -> str "* |-"
 
-let wit_ssrclseq = add_genarg "ssrclseq" pr_clseq
+let wit_ssrclseq = add_genarg "ssrclseq" (fun env sigma -> pr_clseq)
 let pr_clausehyps = pr_list pr_spc pr_wgen
 let pr_ssrclausehyps _ _ _ = pr_clausehyps
 
@@ -1220,7 +1220,7 @@ let pr_fwdkind = function
   | FwdHint (s,_) -> str (s ^ " ") | _ -> str " :=" ++ spc ()
 let pr_fwdfmt (fk, _ : ssrfwdfmt) = pr_fwdkind fk
 
-let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
+let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" (fun env sigma -> pr_fwdfmt)
 
 (* type ssrfwd = ssrfwdfmt * ssrterm *)
 
@@ -1283,11 +1283,11 @@ END
 
 {
 
-let pr_ssrbvar prc _ _ v = prc v
+let pr_ssrbvar env sigma prc _ _ v = prc env sigma v
 
 }
 
-ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY { pr_ssrbvar }
+ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY { pr_ssrbvar env sigma }
 | [ ident(id) ] -> { mkCVar ~loc id }
 | [ "_" ] -> { mkCHole (Some loc) }
 END
@@ -1299,11 +1299,11 @@ let bvar_lname = let open CAst in function
     CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid)
   | { loc = loc } -> CAst.make ?loc Anonymous
 
-let pr_ssrbinder prc _ _ (_, c) = prc c
+let pr_ssrbinder env sigma prc _ _ (_, c) = prc env sigma c
 
 }
 
-ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinder }
+ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinder env sigma }
  | [ ssrbvar(bv) ] ->
    { let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
@@ -1474,11 +1474,11 @@ END
 
 {
 
-let pr_ssrhavefwd _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint prt hint
+let pr_ssrhavefwd env sigma _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint env sigma prt hint
 
 }
 
-ARGUMENT EXTEND ssrhavefwd TYPED AS (ssrfwd * ssrhint) PRINTED BY { pr_ssrhavefwd }
+ARGUMENT EXTEND ssrhavefwd TYPED AS (ssrfwd * ssrhint) PRINTED BY { pr_ssrhavefwd env sigma }
 | [ ":" ast_closure_lterm(t) ssrhint(hint) ] -> { mkFwdHint ":" t, hint }
 | [ ":" ast_closure_lterm(t) ":=" ast_closure_lterm(c) ] -> { mkFwdCast FwdHave ~loc t ~c, nohint }
 | [ ":" ast_closure_lterm(t) ":=" ] -> { mkFwdHintNoTC ":" t, nohint }
@@ -1503,14 +1503,14 @@ let binder_to_intro_id = CAst.(List.map (function
   | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)]
   | _ -> anomaly "ssrbinder is not a binder"))
 
-let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) =
-  pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint
+let pr_ssrhavefwdwbinders env sigma _ _ prt (tr,((hpats, (fwd, hint)))) =
+  pr_hpats hpats ++ pr_fwd fwd ++ pr_hint env sigma prt hint
 
 }
 
 ARGUMENT EXTEND ssrhavefwdwbinders
   TYPED AS (bool * (ssrhpats * (ssrfwd * ssrhint)))
-  PRINTED BY { pr_ssrhavefwdwbinders }
+  PRINTED BY { pr_ssrhavefwdwbinders env sigma }
 | [ ssrhpats_wtransp(trpats) ssrbinder_list(bs) ssrhavefwd(fwd) ] ->
   { let tr, pats = trpats in
     let ((clr, pats), binders), simpl = pats in
@@ -1522,14 +1522,14 @@ END
 
 {
 
-let pr_ssrdoarg prc _ prt (((n, m), tac), clauses) =
-  pr_index n ++ pr_mmod m ++ pr_hintarg prt tac ++ pr_clauses clauses
+let pr_ssrdoarg env sigma prc _ prt (((n, m), tac), clauses) =
+  pr_index n ++ pr_mmod m ++ pr_hintarg env sigma prt tac ++ pr_clauses clauses
 
 }
 
 ARGUMENT EXTEND ssrdoarg
   TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses)
-  PRINTED BY { pr_ssrdoarg }
+  PRINTED BY { pr_ssrdoarg env sigma }
 | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
@@ -1537,22 +1537,22 @@ END
 
 (* type ssrseqarg = ssrindex * (ssrtacarg * ssrtac option) *)
 
-let pr_seqtacarg prt = function
+let pr_seqtacarg env sigma prt = function
   | (is_first, []), _ -> str (if is_first then "first" else "last")
   | tac, Some dtac ->
-    hv 0 (pr_hintarg prt tac ++ spc() ++ str "|| " ++ prt tacltop dtac)
-  | tac, _ -> pr_hintarg prt tac
+    hv 0 (pr_hintarg env sigma prt tac ++ spc() ++ str "|| " ++ prt env sigma tacltop dtac)
+  | tac, _ -> pr_hintarg env sigma prt tac
 
-let pr_ssrseqarg _ _ prt = function
-  | ArgArg 0, tac -> pr_seqtacarg prt tac
-  | i, tac -> pr_index i ++ str " " ++ pr_seqtacarg prt tac
+let pr_ssrseqarg env sigma _ _ prt = function
+  | ArgArg 0, tac -> pr_seqtacarg env sigma prt tac
+  | i, tac -> pr_index i ++ str " " ++ pr_seqtacarg env sigma prt tac
 
 }
 
 (* We must parse the index separately to resolve the conflict with *)
 (* an unindexed tactic.                                            *)
 ARGUMENT EXTEND ssrseqarg TYPED AS (ssrindex * (ssrhintarg * tactic option))
-                          PRINTED BY { pr_ssrseqarg }
+                          PRINTED BY { pr_ssrseqarg env sigma }
 | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" }
 END
 
@@ -2278,7 +2278,7 @@ let pr_rwkind = function
   | RWdef -> str "/"
   | RWeq -> mt ()
 
-let wit_ssrrwkind = add_genarg "ssrrwkind" pr_rwkind
+let wit_ssrrwkind = add_genarg "ssrrwkind" (fun env sigma -> pr_rwkind)
 
 let pr_rule = function
   | RWred s, _ -> pr_simpl s
@@ -2520,13 +2520,13 @@ END
 
 {
 
-let pr_ssrsufffwdwbinders _ _ prt (hpats, (fwd, hint)) =
-  pr_hpats hpats ++ pr_fwd fwd ++ pr_hint prt hint
+let pr_ssrsufffwdwbinders env sigma _ _ prt (hpats, (fwd, hint)) =
+  pr_hpats hpats ++ pr_fwd fwd ++ pr_hint env sigma prt hint
 
 }
 
 ARGUMENT EXTEND ssrsufffwd
-  TYPED AS (ssrhpats * (ssrfwd * ssrhint)) PRINTED BY { pr_ssrsufffwdwbinders }
+  TYPED AS (ssrhpats * (ssrfwd * ssrhint)) PRINTED BY { pr_ssrsufffwdwbinders env sigma }
 | [ ssrhpats(pats) ssrbinder_list(bs)  ":" ast_closure_lterm(t) ssrhint(hint) ] ->
   { let ((clr, pats), binders), simpl = pats in
     let allbs = intro_id_to_binder binders @ bs in
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 7844050272..4a872be6a5 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -14,13 +14,15 @@ open Ltac_plugin
 
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
+val pr_ssrtacarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
+  (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c) -> 'c
 
 val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
+  (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
 
-val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
+val add_genarg : string -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
 (* Parsing witnesses, needed to serialize ssreflect syntax *)
 open Ssrmatching_plugin
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 38f5b7d107..5d8c94e49b 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -57,11 +57,17 @@ let pr_guarded guard prc c =
   let s = Format.flush_str_formatter () ^ "$" in
   if guard s (skip_wschars s 0) then pr_paren prc c else prc c
 
-let prl_constr_expr = Ppconstr.pr_lconstr_expr
+let prl_constr_expr =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Ppconstr.pr_lconstr_expr env sigma
 let pr_glob_constr c = Printer.pr_glob_constr_env (Global.env ()) c
 let prl_glob_constr c = Printer.pr_lglob_constr_env (Global.env ()) c
 let pr_glob_constr_and_expr = function
-  | _, Some c -> Ppconstr.pr_constr_expr c
+  | _, Some c ->
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Ppconstr.pr_constr_expr env sigma c
   | c, None -> pr_glob_constr c
 let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
 
@@ -91,7 +97,10 @@ let pr_simpl = function
 
 (* New terms *)
 
-let pr_ast_closure_term { body } = Ppconstr.pr_constr_expr body
+let pr_ast_closure_term { body } =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Ppconstr.pr_constr_expr env sigma body
 
 let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c)
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 2e1554d496..d3f89147fa 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -198,13 +198,13 @@ type raw_glob_search_about_item =
   | RGlobSearchSubPattern of constr_expr
   | RGlobSearchString of Loc.t * string * string option
 
-let pr_search_item = function
+let pr_search_item env sigma = function
   | RGlobSearchString (_,s,_) -> str s
-  | RGlobSearchSubPattern p -> pr_constr_expr p
+  | RGlobSearchSubPattern p -> pr_constr_expr env sigma p
 
 let wit_ssr_searchitem = add_genarg "ssr_searchitem" pr_search_item
 
-let pr_ssr_search_item _ _ _ = pr_search_item
+let pr_ssr_search_item env sigma _ _ _ = pr_search_item env sigma
 
 (* Workaround the notation API that can only print notations *)
 
@@ -316,7 +316,7 @@ let interp_search_notation ?loc tag okey =
 }
 
 ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem
-  PRINTED BY { pr_ssr_search_item }
+  PRINTED BY { pr_ssr_search_item env sigma }
   | [ string(s) ] -> {  RGlobSearchString (loc,s,None)  }
   | [ string(s) "%" preident(key) ] -> {  RGlobSearchString (loc,s,Some key)  }
   | [ constr_pattern(p) ] -> {  RGlobSearchSubPattern p  }
@@ -324,14 +324,14 @@ END
 
 {
 
-let pr_ssr_search_arg _ _ _ =
-  let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item p in
+let pr_ssr_search_arg env sigma _ _ _ =
+  let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item env sigma p in
   pr_list spc pr_item
 
 }
 
 ARGUMENT EXTEND ssr_search_arg TYPED AS (bool * ssr_searchitem) list
-  PRINTED BY { pr_ssr_search_arg }
+  PRINTED BY { pr_ssr_search_arg env sigma }
   | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> {  (false, p) :: a  }
   | [ ssr_search_item(p) ssr_search_arg(a) ] -> {  (true, p) :: a  }
   | [ ] -> {  []  }
@@ -432,7 +432,7 @@ let interp_search_arg arg =
 
 let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m
 
-let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc
+let wit_ssrmodloc = add_genarg "ssrmodloc" (fun env sigma -> pr_modloc)
 
 let pr_ssr_modlocs _ _ _ ml =
   if ml = [] then str "" else spc () ++ str "in " ++ pr_list spc pr_modloc ml
@@ -491,24 +491,23 @@ END
 
 {
 
-let pr_raw_ssrhintref prc _ _ = let open CAst in function
+let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function
   | { v = CAppExpl ((None, r,x), args) } when isCHoles args ->
-    prc (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args)
-  | { v = CApp ((_, { v = CRef _ }), _) } as c -> prc c
+    prc env sigma (CAst.make @@ CRef (r,x)) ++ str "|" ++ int (List.length args)
+  | { v = CApp ((_, { v = CRef _ }), _) } as c -> prc env sigma c
   | { v = CApp ((_, c), args) } when isCxHoles args ->
-    prc c ++ str "|" ++ int (List.length args)
-  | c -> prc c
+    prc env sigma c ++ str "|" ++ int (List.length args)
+  | c -> prc env sigma c
 
-let pr_rawhintref c =
-  let _, env = Pfedit.get_current_context () in
+let pr_rawhintref env sigma c =
   match DAst.get c with
   | GApp (f, args) when isRHoles args ->
     pr_glob_constr_env env f ++ str "|" ++ int (List.length args)
   | _ -> pr_glob_constr_env env c
 
-let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c
+let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c
 
-let pr_ssrhintref prc _ _ = prc
+let pr_ssrhintref env sigma prc _ _ = prc env sigma
 
 let mkhintref ?loc c n = match c.CAst.v with
   | CRef (r,x) -> CAst.make ?loc @@ CAppExpl ((None, r, x), mkCHoles ?loc n)
@@ -518,9 +517,9 @@ let mkhintref ?loc c n = match c.CAst.v with
 
 ARGUMENT EXTEND ssrhintref
   TYPED AS constr
-  PRINTED BY { pr_ssrhintref }
-  RAW_PRINTED BY { pr_raw_ssrhintref }
-  GLOB_PRINTED BY { pr_glob_ssrhintref }
+  PRINTED BY { pr_ssrhintref env sigma }
+  RAW_PRINTED BY { pr_raw_ssrhintref env sigma }
+  GLOB_PRINTED BY { pr_glob_ssrhintref env sigma }
   | [ constr(c) ] -> {  c  }
   | [ constr(c) "|" natural(n) ] -> {  mkhintref ~loc c n  }
 END
@@ -559,19 +558,22 @@ END
 
 {
 
-let print_view_hints kind l =
+let print_view_hints env sigma kind l =
   let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in
-  let pp_hints = pr_list spc pr_rawhintref l in
+  let pp_hints = pr_list spc (pr_rawhintref env sigma) l in
   Feedback.msg_info  (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ())
 
 }
 
 VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
 | [ "Print" "Hint" "View" ssrviewpos(i) ] ->
-  { match i with
-    | Some k -> print_view_hints k (Ssrview.AdaptorDb.get k)
+  {
+    let sigma, env = Pfedit.get_current_context () in
+    match i with
+    | Some k ->
+      print_view_hints env sigma k (Ssrview.AdaptorDb.get k)
     | None ->
-        List.iter (fun k -> print_view_hints k (Ssrview.AdaptorDb.get k))
+        List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k))
           [ Ssrview.AdaptorDb.Forward;
             Ssrview.AdaptorDb.Backward;
             Ssrview.AdaptorDb.Equivalence ]