diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index edbacbebe..bdc6cb72a 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -558,7 +558,7 @@ let nf_betadeltaiota env sigma = du type checking : (fun x => x + x) M *) -let rec whd_betaiota_preserving_vm_cast env sigma t = +let whd_betaiota_preserving_vm_cast env sigma t = let rec stacklam_var subst t stack = match (decomp_stack stack,kind_of_term t) with | Some (h,stacktl), Lambda (_,_,c) -> |