diff options
Diffstat (limited to 'stm/lemmas.ml')
-rw-r--r-- | stm/lemmas.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 004dd6801..b1b8aa288 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -241,7 +241,7 @@ let save_remaining_recthms { locality; polymorphic; object_kind } let k = IsAssumption Conjectural in let c = SectionLocalAssum { type_context = (t_i,ctx); polymorphic; - binding_kind = impl } + implicit_status = impl } in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) |