diff options
| author | Maxime Dénès | 2017-05-20 01:31:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-20 01:31:20 +0200 |
| commit | 7dc84057e3596b1c3f6ec869daebcfa8747f5c12 (patch) | |
| tree | 0ac6c9286745aee5c42344e91750a45a33b68f5f | |
| parent | a78bfb93a6ece86b1f56f41d12d900d369444451 (diff) | |
| parent | fa530442ba05e9b60efff9c726616ae00d6d09e7 (diff) | |
Merge PR#627: Obligations shrinking: shrink abstraction too
| -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 5233fab151..24cb9c886e 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 = |