diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-05-04 18:30:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-05-11 15:15:25 +0200 |
| commit | fa530442ba05e9b60efff9c726616ae00d6d09e7 (patch) | |
| tree | 1751d17365c02e301a90cd9b63b8a52e68ccbbfc /vernac/obligations.ml | |
| parent | 8e6d03830e9c53f641626e29886eb07c705f7608 (diff) | |
Obligations shrinking: shrink abstraction too
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 = |