aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/lemmas.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/lemmas.ml')
-rw-r--r--stm/lemmas.ml2
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)