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

1 files changed, 12 insertions, 13 deletions

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