diff options
| -rw-r--r-- | engine/evd.ml | 5 | ||||
| -rw-r--r-- | engine/evd.mli | 5 | ||||
| -rw-r--r-- | interp/declare.ml | 14 | ||||
| -rw-r--r-- | interp/declare.mli | 2 | ||||
| -rw-r--r-- | kernel/entries.ml | 5 | ||||
| -rw-r--r-- | tactics/abstract.ml | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 4 |
7 files changed, 21 insertions, 16 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 508ac0f65a..34de2f41bb 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -430,9 +430,12 @@ type evar_flags = restricted_evars : Evar.t Evar.Map.t; typeclass_evars : Evar.Set.t } +type side_effect_role = +| Schema of inductive * string + type side_effects = { seff_private : Safe_typing.private_constants; - seff_roles : Entries.side_effect_role Cmap.t; + seff_roles : side_effect_role Cmap.t; } type evar_map = { diff --git a/engine/evd.mli b/engine/evd.mli index 46b69de232..5478431e14 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -307,9 +307,12 @@ val dependent_evar_ident : Evar.t -> evar_map -> Id.t (** {5 Side-effects} *) +type side_effect_role = +| Schema of inductive * string + type side_effects = { seff_private : Safe_typing.private_constants; - seff_roles : Entries.side_effect_role Cmap.t; + seff_roles : side_effect_role Cmap.t; } val empty_side_effects : side_effects 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 -> diff --git a/kernel/entries.ml b/kernel/entries.ml index adb3f6bd29..45b11e97ba 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -107,8 +107,3 @@ type module_entry = | MType of module_params_entry * module_struct_entry | MExpr of module_params_entry * module_struct_entry * module_struct_entry option - -(** Not used by the kernel. *) -type side_effect_role = - | Subproof - | Schema of inductive * string diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 0547071519..967b0ef418 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl + Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index eaff889dbf..539fe31416 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -145,7 +145,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let role = Entries.Schema (ind, kind) in + let role = Evd.Schema (ind, kind) in let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; const, Evd.concat_side_effects neff eff @@ -163,7 +163,7 @@ let define_mutual_scheme_base kind suff f mode names mind = try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let fold i effs id cl = - let role = Entries.Schema ((mind, i), kind)in + let role = Evd.Schema ((mind, i), kind)in let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in (Evd.concat_side_effects neff effs, cst) in |