diff options
| author | Maxime Dénès | 2020-05-14 16:33:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-05-14 16:33:15 +0200 |
| commit | 81fba800a97955368791df115e807cde66eff19c (patch) | |
| tree | c0cb601061912a95a8b5ad031f0378a1e479320b /pretyping/typing.ml | |
| parent | 8dd5c47007817c104d57a449409a6b9c6f8ef12e (diff) | |
| parent | 101d898869ffa07fc772b303e3dbb7ecd860386b (diff) | |
Merge PR #11922: No more local reduction functions in Reductionops.
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
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 |