diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b16f1a9ed..4c87b4e7e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1015,7 +1015,7 @@ let adjust_impossible_cases pb pred tomatch submat = | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin let evd, default = use_unit_judge !(pb.evdref) in - pb.evdref := Evd.define evk (EConstr.Unsafe.to_constr default.uj_type) evd + pb.evdref := Evd.define evk default.uj_type evd end; add_assert_false_case pb tomatch | _ -> |