diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 15:55:54 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-02 15:55:54 +0100 |
| commit | e6353e9ef6542b444391a46d9557ebf3a6443947 (patch) | |
| tree | 5cdc9ba397db963006d747716321c029b194eba8 /proofs | |
| parent | 1d9e15c99a90311f8e082fb39615ae1c4aee8084 (diff) | |
Reductionops.nf_* now take an environment.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 4 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 16798a1d5..9e06d913b 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -498,7 +498,7 @@ let clenv_unify_binding_type clenv c t u = let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in - let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in + let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in let c = EConstr.Unsafe.to_constr c in { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } diff --git a/proofs/logic.ml b/proofs/logic.ml index 1d86a0909..5ff5fa38a 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -334,7 +334,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = else match kind trm with | Meta _ -> - let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in + let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in if !check && occur_meta sigma conclty then raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in @@ -416,7 +416,7 @@ and mk_hdgoals sigma goal goalacc trm = match kind trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; - let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in + let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index d41541251..bdcb4868b 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -87,7 +87,7 @@ let pf_e_reduce = pf_apply let pf_whd_all = pf_reduce whd_all let pf_hnf_constr = pf_reduce hnf_constr let pf_nf = pf_reduce simpl -let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) +let pf_nf_betaiota = pf_reduce nf_betaiota let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) let pf_unsafe_type_of = pf_reduce unsafe_type_of |