diff options
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e0520216b..62c594389 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -631,6 +631,16 @@ let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst) +let it_mkLambda_or_LetIn_or_clean t ctx = + let open Context.Rel.Declaration in + let fold t decl = + if is_local_assum decl then mkLambda_or_LetIn decl t + else + if noccurn 1 t then subst1 mkProp t + else mkLambda_or_LetIn decl t + in + Context.Rel.fold_inside fold ctx ~init:t + let declare_obligation prg obl body ty uctx = let body = prg.prg_reduce body in let ty = Option.map prg.prg_reduce ty in @@ -664,7 +674,7 @@ let declare_obligation prg obl body ty uctx = if poly then Some (DefinedObl constant) else - Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) } + Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) } let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind notations obls impls kind reduce hook = |