diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 40c65b56f..7bb016d34 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -230,7 +230,7 @@ let declare_assumption is_coe assumption_kind (c,ctx) pl imps impl nl (_,ident) | Discharge when Lib.sections_are_opened () -> let entry = SectionLocalAssum { type_context = (c,ctx); polymorphic; - binding_kind = impl } + implicit_status = impl } in let decl = (Lib.cwd(), entry, IsAssumption kind) in let _ = declare_variable ident decl in |