[plugins] [ssr] Adapt to removal of imperative proof state.

7 files changed, 43 insertions, 34 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 6956120a6a..0ca7e904da 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 env sigma (EConstr.Unsafe.to_constr t) ++
+        (pr_econstr_pat env sigma 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 94f7d24242..350bb9019e 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -239,8 +239,10 @@ 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 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 () =
+    let sigma = project gl in
+    ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim));
+    ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in
   let inf_deps_r = match EConstr.kind_of_type (project gl) elimty with
     | AtomicType (_, args) -> List.rev (Array.to_list args)
     | _ -> assert false in
@@ -304,7 +306,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
    * 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 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 pp_inf_pat gl (_,_,t,_) = pr_econstr_pat env (project gl) (fire_subst gl t) in
   let patterns, clr, gl =
     let rec loop patterns clr i = function
       | [],[] -> patterns, clr, gl
@@ -318,7 +320,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 env (project gl) (EConstr.Unsafe.to_constr c)));
+          ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c));
           loop (patterns @ [i, mkTpat gl c, c, allocc]) 
             clr (i+1) ([], inf_deps)
       | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in
@@ -341,7 +343,7 @@ 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 env (project gl) (EConstr.Unsafe.to_constr (fire_subst gl inf_t))++spc()++ str"doesn't") in
+      spc()++pr_econstr_pat env (project gl) (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
@@ -426,7 +428,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 env (project gl) (EConstr.Unsafe.to_constr pat)++spc()++
+      errorstrm Pp.(str"Pattern"++spc()++pr_econstr_pat env (project gl) 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 902098c8ce..5abbc214de 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -205,7 +205,7 @@ let rec get_evalref env sigma c = match EConstr.kind sigma c with
   | 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 env sigma (EConstr.Unsafe.to_constr c) ++ str " is not unfoldable")
+  | _ -> errorstrm Pp.(str "The term " ++ pr_econstr_pat (Global.env ()) sigma 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
@@ -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 env sigma (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)),
+        ++ pr_econstr_pat env sigma0 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 env sigma (EConstr.Unsafe.to_constr t))),
+          pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_econstr_pat env sigma 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 env0 sigma (EConstr.Unsafe.to_constr t)) in
+    with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in
   let _ = conclude () in
   Proofview.V82.of_tactic (convert_concl concl) gl
 ;;
@@ -415,7 +415,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 (pf_env gl) (project gl) (EConstr.Unsafe.to_constr (snd sr))
+        errorstrm Pp.(str "no cast from " ++ pr_econstr_pat (pf_env gl) (project gl) (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
@@ -433,9 +433,8 @@ let rwcltac cl rdx dir sr gl =
       if occur_existential (project gl) (Tacmach.pf_concl gl)
       then errorstrm Pp.(str "Rewriting impacts evars" ++ error)
       else errorstrm Pp.(str "Dependent type error in rewrite of "
-        ++ pr_constr_env (pf_env gl) (project gl)
-          (Term.mkNamedLambda (make_annot pattern_id Sorts.Relevant)
-             (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))
+        ++ pr_econstr_env (pf_env gl) (project gl)
+          (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl)
         ++ error)
   in
   tclTHEN cvtac' rwtac gl
@@ -480,7 +479,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 env sigma (EConstr.Unsafe.to_constr t)));
+      ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t));
       match EConstr.kind sigma t with
       | Prod (_, xt, at) ->
         let sigma = Evd.create_evar_defs sigma in
@@ -539,8 +538,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 env sigma (EConstr.Unsafe.to_constr t)
-                        ++ spc() ++ str "in rule " ++ pr_constr_pat env sigma (EConstr.Unsafe.to_constr (snd rule)))
+        else errorstrm Pp.(str "not a rewritable relation: " ++ pr_econstr_pat env sigma t
+                        ++ spc() ++ str "in rule " ++ pr_econstr_pat env sigma (snd rule))
         in
     let sigma, r = rule in
     let t = Retyping.get_type_of env sigma r in
@@ -554,9 +553,9 @@ let rwrxtac occ rdx_pat dir rule gl =
   let find_rule rdx =
     let rec rwtac = function
       | [] ->
-        errorstrm Pp.(str "pattern " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr rdx) ++
+        errorstrm Pp.(str "pattern " ++ pr_econstr_pat env (project gl) rdx ++
                    str " does not match " ++ pr_dir_side dir ++
-                   str " of " ++ pr_constr_pat env (project gl) (EConstr.Unsafe.to_constr (snd rule)))
+                   str " of " ++ pr_econstr_pat env (project gl) (snd rule))
       | (d, r, lhs, rhs) :: rs ->
         try
           let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index be9586fdd7..3cadc92bcc 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 env sigma (EConstr.Unsafe.to_constr c)++spc()++str"did not match and has holes."++spc()++
+    pr_econstr_pat env sigma 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/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index d3f89147fa..0a0d9b12fa 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -566,17 +566,21 @@ let print_view_hints env sigma kind l =
 }
 
 VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
-| [ "Print" "Hint" "View" ssrviewpos(i) ] ->
+| ![proof] [ "Print" "Hint" "View" ssrviewpos(i) ] ->
   {
-    let sigma, env = Pfedit.get_current_context () in
-    match i with
+    fun ~pstate ->
+    (* XXX this is incorrect *)
+    let sigma, env = Option.cata Pfedit.get_current_context
+        (let e = Global.env () in Evd.from_env e, e) pstate in
+    (match i with
     | Some k ->
       print_view_hints env sigma k (Ssrview.AdaptorDb.get k)
     | None ->
         List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k))
           [ Ssrview.AdaptorDb.Forward;
             Ssrview.AdaptorDb.Backward;
-            Ssrview.AdaptorDb.Equivalence ]
+            Ssrview.AdaptorDb.Equivalence ]);
+    pstate
   }
 END
 
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 5eb106cc26..4b5fa7bf27 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -373,6 +373,12 @@ let pr_constr_pat env sigma c0 =
     if isEvar c then hole_var else map wipe_evar c in
   pr_constr_env env sigma (wipe_evar c0)
 
+let ehole_var = EConstr.mkVar (Id.of_string "_")
+let pr_econstr_pat env sigma c0 =
+  let rec wipe_evar c = let open EConstr in
+    if isEvar sigma c then ehole_var else map sigma wipe_evar c in
+  pr_econstr_env env sigma (wipe_evar c0)
+
 (* Turn (new) evars into metas *)
 let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
   let ise = ref ise0 in
@@ -694,8 +700,7 @@ let source env = match upats_origin, upats with
       (if fixed_upat ise p then str"term " else str"partial term ") ++
       pr_constr_pat env ise (p2t p) ++ spc()
   | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
-      pr_constr_pat env ise rule ++ fnl() ++ ws 4 ++
-      pr_constr_pat env ise (p2t p) ++ fnl()
+      pr_constr_pat env ise rule ++ fnl() ++ ws 4 ++ pr_constr_pat env ise (p2t p) ++ fnl()
   | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ 
       pr_constr_pat env ise rule ++ spc()
   | _, [] | None, _::_::_ ->
@@ -732,13 +737,13 @@ let rec uniquize = function
       env, 0, uniquize (instances ())
     | NoMatch when (not raise_NoMatch) ->
       if !failed_because_of_TC then
-        errorstrm (source env++strbrk"matches but type classes inference fails")
+        errorstrm (source env ++ strbrk"matches but type classes inference fails")
       else
         errorstrm (source env ++ str "does not match any subterm of the goal")
     | NoProgress when (not raise_NoMatch) ->
         let dir = match upats_origin with Some (d,_) -> d | _ ->
           CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in
-        errorstrm (str"all matches of "++source env++
+        errorstrm (str"all matches of "++ source env ++
           str"are equal to the " ++ pr_dir_side (inv_dir dir))
     | NoProgress -> raise NoMatch);
   let sigma, _, ({up_f = pf; up_a = pa} as u) =
@@ -823,7 +828,7 @@ let pr_pattern_aux pr_constr = function
   | E_As_X_In_T (e,x,t) ->
       pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t
 let pp_pattern env (sigma, p) =
-  pr_pattern_aux (fun t -> pr_constr_pat env sigma (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p
+  pr_pattern_aux (fun t -> pr_econstr_pat env sigma (pi3 (nf_open_term sigma sigma (EConstr.of_constr t)))) p
 let pr_cpattern = pr_term
 
 let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern)
@@ -1253,10 +1258,8 @@ let fill_occ_term env cl occ sigma0 (sigma, t) =
     if sigma' != sigma0 then raise NoMatch
     else cl, (Evd.merge_universe_context sigma' uc, t')
   with _ ->
-    errorstrm (str "partial term " ++
-               pr_constr_pat env sigma
-                (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) ++
-               str " does not match any subterm of the goal")
+    errorstrm (str "partial term " ++ pr_econstr_pat env sigma t
+            ++ str " does not match any subterm of the goal")
 
 let pf_fill_occ_term gl occ t =
   let sigma0 = project gl and env = pf_env gl and concl = pf_concl gl in
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 1143bcc813..25975c84e8 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -223,6 +223,7 @@ val id_of_pattern : pattern -> Names.Id.t option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.Id.t -> cpattern
 val pr_constr_pat : env -> evar_map -> constr -> Pp.t
+val pr_econstr_pat : env -> evar_map -> econstr -> Pp.t
 val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma
 val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma