diff options
| author | Emilio Jesus Gallego Arias | 2018-10-04 23:21:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-07 19:41:45 +0200 |
| commit | dac8b249e95d376de587d7b527fd17f70e4942fc (patch) | |
| tree | 74be87f519c5fbd4c5f35355749f7050a2cb1da0 /plugins | |
| parent | 9a13a86115823a24738489f0b11b692f4ed065ad (diff) | |
[api] Deprecate `evar_map` ref combinators.
All the `evar_map` APIs were deprecated in 8.9, thus we deprecate the
combinators to discourage this style of programming.
Still a few places do use imperative style, but they are pretty
localized and should be cleaned up separately.
As these are the last bits of `e_` API remaining this PR closes #6342.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 839915631d..f7094ebe51 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -322,7 +322,8 @@ let generate_functional_principle (evd: Evd.evar_map ref) try let f = funs.(i) in - let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in + let sigma, type_sort = Evd.fresh_sort_in_family !evd InType in + evd := sigma; let new_sorts = match sorts with | None -> Array.make (Array.length funs) (type_sort) @@ -507,8 +508,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x - ) + let sigma, fs = Evd.fresh_sort_in_family !evd x in + evd := sigma; fs + ) fas in (* We create the first priciple by tactic *) |