diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 64ad1801f0..540db1c815 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1024,6 +1024,7 @@ let rec generalize_problem names pb = function | [] -> pb | i::l -> let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in + let d = on_pi3 (whd_betaiota !(pb.evdref)) d in (* for better rendering *) let pb' = generalize_problem names pb l in let tomatch = lift_tomatch_stack 1 pb'.tomatch in let tomatch = regeneralize_index_tomatch (i+1) tomatch in |