diff options
| author | Pierre-Marie Pédrot | 2019-06-05 10:35:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-11 16:59:07 +0200 |
| commit | e753855167e5629775b604128c6efc9d58ee626c (patch) | |
| tree | 7abdebb08679b76a80cf9d1a36f05b91a538c223 /plugins | |
| parent | 3d162ca9095ff9299be5cc8847636a36b8e49f1e (diff) | |
Remove the side-effect role from the kernel.
We move the role data into the evarmap instead.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/derive/derive.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 |
4 files changed, 6 insertions, 6 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 79d1c7520f..aad3967f6d 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -12,8 +12,8 @@ open Constr open Context open Context.Named.Declaration -let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) - : Safe_typing.private_constants Entries.const_entry_body = +let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body) + : Evd.side_effects Entries.const_entry_body = Future.chain x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d1e540cceb..5363dc9a02 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -471,7 +471,7 @@ let get_funs_constant mp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_constants definition_entry list = +let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects definition_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -597,7 +597,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ in {const with const_entry_body = - (Future.from_val (Safe_typing.mk_pure_proof princ_body)); + (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); const_entry_type = Some scheme_type } ) diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 97f9acdb3a..759c522820 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -34,7 +34,7 @@ val generate_functional_principle : exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list + (pconstant*Sorts.family) list -> Evd.side_effects Entries.definition_entry list val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 9670cf1fa7..4078c34331 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -44,7 +44,7 @@ val jmeq_refl : unit -> EConstr.constr val save : Id.t - -> Safe_typing.private_constants Entries.definition_entry + -> Evd.side_effects Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> UState.t -> Decl_kinds.goal_kind |