From e6353e9ef6542b444391a46d9557ebf3a6443947 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Feb 2018 15:55:54 +0100 Subject: Reductionops.nf_* now take an environment. --- vernac/himsg.ml | 22 +++++++++++----------- vernac/vernacentries.ml | 2 +- 2 files changed, 12 insertions(+), 12 deletions(-) (limited to 'vernac') diff --git a/vernac/himsg.ml b/vernac/himsg.ml index e8c5aeedd..f00c1e604 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -83,12 +83,12 @@ let rec contract3' env sigma a b c = function (** Ad-hoc reductions *) -let j_nf_betaiotaevar sigma j = +let j_nf_betaiotaevar env sigma j = { uj_val = j.uj_val; - uj_type = Reductionops.nf_betaiota sigma j.uj_type } + uj_type = Reductionops.nf_betaiota env sigma j.uj_type } -let jv_nf_betaiotaevar sigma jl = - Array.map (fun j -> j_nf_betaiotaevar sigma j) jl +let jv_nf_betaiotaevar env sigma jl = + Array.map (fun j -> j_nf_betaiotaevar env sigma j) jl (** Printers *) @@ -258,7 +258,7 @@ let explain_number_branches env sigma cj expn = str "expects " ++ int expn ++ str " branches." let explain_ill_formed_branch env sigma c ci actty expty = - let simp t = Reductionops.nf_betaiota sigma t in + let simp t = Reductionops.nf_betaiota env sigma t in let env = make_all_name_different env sigma in let pc = pr_leconstr_env env sigma c in let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in @@ -295,8 +295,8 @@ let explain_unification_error env sigma p1 p2 = function | NotSameArgSize | NotSameHead | NoCanonicalStructure -> (* Error speaks from itself *) [] | ConversionFailed (env,t1,t2) -> - let t1 = Reductionops.nf_betaiota sigma t1 in - let t2 = Reductionops.nf_betaiota sigma t2 in + let t1 = Reductionops.nf_betaiota env sigma t1 in + let t2 = Reductionops.nf_betaiota env sigma t2 in if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else let env = make_all_name_different env sigma in if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then @@ -336,8 +336,8 @@ let explain_unification_error env sigma p1 p2 = function let explain_actual_type env sigma j t reason = let env = make_all_name_different env sigma in - let j = j_nf_betaiotaevar sigma j in - let t = Reductionops.nf_betaiota sigma t in + let j = j_nf_betaiotaevar env sigma j in + let t = Reductionops.nf_betaiota env sigma t in (** Actually print *) let pe = pr_ne_context_of (str "In environment") env sigma in let pc = pr_leconstr_env env sigma (Environ.j_val j) in @@ -351,8 +351,8 @@ let explain_actual_type env sigma j t reason = ppreason ++ str ".") let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = - let randl = jv_nf_betaiotaevar sigma randl in - let actualtyp = Reductionops.nf_betaiota sigma actualtyp in + let randl = jv_nf_betaiotaevar env sigma randl in + let actualtyp = Reductionops.nf_betaiota env sigma actualtyp in let env = make_all_name_different env sigma in let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in let nargs = Array.length randl in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1a02a22a5..fb125317e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1587,7 +1587,7 @@ let vernac_check_may_eval ~atts redexp glopt rc = | None -> let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in - let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in + let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma' j.Environ.uj_type } in Feedback.msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ Printer.pr_universe_ctx_set sigma uctx) -- cgit v1.2.3