diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-06 20:08:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-07 00:56:23 +0200 |
| commit | b44b68ec704df75f684e3393980f3518caf1a506 (patch) | |
| tree | ac14d8de80f65597b43e63bf10a3431b83b14939 /kernel/reduction.ml | |
| parent | 3d52830b4876dadb985115a2ffeff6c0b77ca33d (diff) | |
In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in MathClasses).
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1e6f157ab..a4d8872fe 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -758,7 +758,7 @@ let dest_prod env = in decrec env empty_rel_context -(* The same but preserving lets *) +(* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = let rty = whd_betadeltaiota_nolet env ty in @@ -770,7 +770,10 @@ let dest_prod_assum env = let d = (x,Some b,t) in prodec_rec (push_rel d env) (add_rel_decl d l) c | Cast (c,_,_) -> prodec_rec env l c - | _ -> l,rty + | _ -> + let rty' = whd_betadeltaiota env rty in + if Term.eq_constr rty' rty then l, rty + else prodec_rec env l rty' in prodec_rec env empty_rel_context |