diff options
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 786169f409..17c2862cad 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -44,7 +44,6 @@ val declare_definition -> scope:locality -> kind:Decls.logical_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> ?should_suggest:bool -> UnivNames.universe_binders -> Evd.side_effects Declare.proof_entry -> Impargs.manual_implicits |