diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-10 10:31:59 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-10 10:32:25 +0200 |
| commit | c88f47195955beb615d15dd9d57e4de20e5e3a52 (patch) | |
| tree | 824ebe4739ee767a5c452f32d603510cf14db91a /pretyping | |
| parent | 7ed370257e576dd084f89eae52fcc2135d4fbee3 (diff) | |
Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c9d4e388d..f4b32ee77 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1375,7 +1375,10 @@ let splay_prod_assum env sigma = prodec_rec (push_rel (x, Some b, t) env) (add_rel_decl (x, Some b, t) l) c | Cast (c,_,_) -> prodec_rec env l c - | _ -> l,t + | _ -> + let t' = whd_betadeltaiota env sigma t in + if Term.eq_constr t t' then l,t + else prodec_rec env l t' in prodec_rec env empty_rel_context |