diff options
| author | Pierre-Marie Pédrot | 2019-06-08 16:50:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-11 16:59:08 +0200 |
| commit | 929ecfe0cd8cd3edec41416491e286e4c105ffa6 (patch) | |
| tree | 74acaf09aae9dec751c430e4c8bb0127b06cc363 /interp | |
| parent | e753855167e5629775b604128c6efc9d58ee626c (diff) | |
Move the side-effect role out of Entries into Evd.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 14 | ||||
| -rw-r--r-- | interp/declare.mli | 2 |
2 files changed, 10 insertions, 6 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index dce855bbbc..17de06ed57 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -140,8 +140,8 @@ let register_constant kn kind local = let register_side_effect (c, role) = let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in match role with - | Subproof -> () - | Schema (ind, kind) -> !declare_scheme kind [|ind,c|] + | None -> () + | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|] let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types @@ -156,7 +156,7 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types let get_roles export eff = let map c = - let role = try Cmap.find c eff.Evd.seff_roles with Not_found -> Subproof in + let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in (c, role) in List.map map export @@ -199,11 +199,15 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefault let () = register_constant kn kind local in kn -let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = +let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = let kn, eff, export = define_constant ~side_effect:EffectEntry id cd in let () = assert (List.is_empty export) in let () = register_constant kn kind local in - let eff = { Evd.seff_private = eff; Evd.seff_roles = Cmap.singleton kn role } in + let seff_roles = match role with + | None -> Cmap.empty + | Some r -> Cmap.singleton kn r + in + let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff let declare_definition ?(internal=UserIndividualRequest) diff --git a/interp/declare.mli b/interp/declare.mli index ed76f0a284..e2485d7cf0 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -56,7 +56,7 @@ val declare_constant : ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t val declare_private_constant : - role:side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects + ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> |