diff options
Diffstat (limited to 'tactics/declare.mli')
| -rw-r--r-- | tactics/declare.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/declare.mli b/tactics/declare.mli index 692eca8dde..0a2332748c 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -58,7 +58,7 @@ val definition_entry : ?fix_exn:Future.fix_exn -> internal specify if the constant has been created by the kernel or by the user, and in the former case, if its errors should be silent *) val declare_constant : - ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t + ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t val declare_private_constant : ?role:Evd.side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects |