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 89b41076f7..4ae9f6c7ae 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -23,7 +23,7 @@ open Entries type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } type 'a constant_entry = | DefinitionEntry of 'a Proof_global.proof_entry |