diff options
| author | Maxime Dénès | 2019-04-05 11:02:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:44 +0200 |
| commit | f6dc8b19760aaf0cc14e6d9eb2d581ba1a05a762 (patch) | |
| tree | c8301ee07c73e4ef725659ff84d27d958584e5b9 /pretyping/evarsolve.ml | |
| parent | ff07d0f499dcc8876b2b222bf861e9de89315a05 (diff) | |
Remove calls to Global.env from Evarsolve
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a4a078bfa0..6d2d07d1dc 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -73,11 +73,11 @@ let normalize_evar evd ev = | Evar (evk,args) -> (evk,args) | _ -> assert false -let get_polymorphic_positions sigma f = +let get_polymorphic_positions env sigma f = let open Declarations in match EConstr.kind sigma f with - | Ind (ind, u) | Construct ((ind, _), u) -> - let mib,oib = Global.lookup_inductive ind in + | Ind (ind, u) | Construct ((ind, _), u) -> + let mib,oib = Inductive.lookup_mind_specif env ind in (match oib.mind_arity with | RegularArity _ -> assert false | TemplateArity templ -> templ.template_param_levels) @@ -128,7 +128,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) let rec refresh_term_evars ~onevars ~top t = match EConstr.kind !evdref t with | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f -> - let pos = get_polymorphic_positions !evdref f in + let pos = get_polymorphic_positions env !evdref f in refresh_polymorphic_positions args pos; t | App (f, args) when top && isEvar !evdref f -> let f' = refresh_term_evars ~onevars:true ~top:false f in |