diff options
| author | Pierre-Marie Pédrot | 2019-06-24 13:24:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:51:01 +0200 |
| commit | 803c1dbf2de4e4fe1e447a69b9e5c48d19a72f5f (patch) | |
| tree | 14a3c6edead32f558a7703313413565483b9ba8c /tactics/declare.ml | |
| parent | 82bccc5d62cbdcf0d79d8a85c98ca19823a33629 (diff) | |
Remove the internal_flag argument from Declare API.
It was never used actually.
Diffstat (limited to 'tactics/declare.ml')
| -rw-r--r-- | tactics/declare.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index 4a4e2cf60a..27c2d089f6 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -233,7 +233,7 @@ let define_constant ~side_effect id cd = let kn, eff = Global.add_constant ~side_effect ~in_section id decl in kn, eff, export -let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) = +let declare_constant ?(local = ImportDefaultBehavior) id (cd, kind) = let () = check_exists id in let kn, (), export = define_constant ~side_effect:PureEntry id cd in (* Register the libobjects attached to the constants and its subproofs *) @@ -241,7 +241,7 @@ 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 ?(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 @@ -252,13 +252,13 @@ let declare_private_constant ?role ?(internal=UserIndividualRequest) ?(local = I let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff -let declare_definition ?(internal=UserIndividualRequest) +let declare_definition ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior) id ?types (body,univs) = let cb = definition_entry ?types ~univs ~opaque body in - declare_constant ~internal ~local id + declare_constant ~local id (DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of section variables and local definitions *) |