3 files changed, 8 insertions, 5 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e8257b5dba..01e8daf82d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -950,7 +950,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
   let open EConstr in
   if n = 0 then
     let args = List.rev args in
-     (if beta then Reductionops.whd_beta sigma else fun x -> x)
+     (if beta then Reductionops.whd_beta env sigma else fun x -> x)
       (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma
   else match kind_of_type sigma ty with
   | ProdType (_, src, tgt) ->
@@ -1065,11 +1065,12 @@ end
 let introid ?(orig=ref Anonymous) name =
   let open Proofview.Notations in
   Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let g = Proofview.Goal.concl gl in
    match EConstr.kind sigma g with
    | App (hd, _) when EConstr.isLambda sigma hd ->
-      convert_concl_no_check (Reductionops.whd_beta sigma g)
+      convert_concl_no_check (Reductionops.whd_beta env sigma g)
    | _ -> Tacticals.New.tclIDTAC
   end <*>
     (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name))
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ab07dd5be9..29a9c65561 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -281,7 +281,7 @@ let unfoldintac occ rdx t (kt,_) =
           | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a)
           | Proj _ when same_proj sigma0 c t -> body env t c
           | _ ->
-            let c = Reductionops.whd_betaiotazeta sigma0 c in
+            let c = Reductionops.whd_betaiotazeta env sigma0 c in
             match EConstr.kind sigma0 c with
             | Const _ when EConstr.eq_constr sigma0 c t -> body env t t
             | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a)
@@ -516,7 +516,7 @@ let rwprocess_rule env dir rule =
     let rec loop d sigma r t0 rs red =
       let t =
         if red = 1 then Tacred.hnf_constr env sigma t0
-        else Reductionops.whd_betaiotazeta sigma t0 in
+        else Reductionops.whd_betaiotazeta env sigma t0 in
       ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t));
       match EConstr.kind sigma t with
       | Prod (_, xt, at) ->
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 88a3e85211..ad0a31622c 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -194,9 +194,11 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
       Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
     tclUNIT (env,sigma,term)
   with e ->
+    (* XXX this is another catch all! *)
+    let e, info = Exninfo.capture e in
     Ssrprinters.ppdebug (lazy
     Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
-     tclZERO e
+    tclZERO ~info e
 end
 
 (* Commits the term to the monad *)