diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 5 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 4 |
2 files changed, 5 insertions, 4 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e05c4c26dd..62d4adca43 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -947,7 +947,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) -> @@ -1062,11 +1062,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) -> |