From fa530442ba05e9b60efff9c726616ae00d6d09e7 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 4 May 2017 18:30:38 +0200 Subject: Obligations shrinking: shrink abstraction too --- vernac/obligations.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'vernac/obligations.ml') 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 = -- cgit v1.2.3