diff options
| author | Pierre-Marie Pédrot | 2019-03-14 19:00:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-10 15:03:19 +0200 |
| commit | 2a79abc613bdf19b53685a40c993f964455904fe (patch) | |
| tree | c0fd8ab20f683c3141934d060852dcda0d569f00 /pretyping/typing.ml | |
| parent | aab47903fb2d3e0085b03d5ade94f4ae644cd76c (diff) | |
No more local reduction functions in Reductionops.
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 99a35849e0..f0882d4594 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -29,11 +29,11 @@ open Context.Rel.Declaration module GR = Names.GlobRef -let meta_type evd mv = +let meta_type env evd mv = let ty = try Evd.meta_ftype evd mv with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in - meta_instance evd ty + meta_instance env evd ty let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in @@ -175,7 +175,7 @@ let type_case_branches env sigma (ind,largs) pj c = let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in - let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in + let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in sigma, (lc, ty, Sorts.relevance_of_sort ps) let judge_of_case env sigma ci pj cj lfj = @@ -335,7 +335,7 @@ let rec execute env sigma cstr = let cstr = whd_evar sigma cstr in match EConstr.kind sigma cstr with | Meta n -> - sigma, { uj_val = cstr; uj_type = meta_type sigma n } + sigma, { uj_val = cstr; uj_type = meta_type env sigma n } | Evar ev -> let ty = EConstr.existential_type sigma ev in |