diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 81bd6987fe..dc3ea869c1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -479,7 +479,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let f = it_mkLambda_or_LetIn fj.uj_val fsign in let v = let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env LetStyle mis in + let ci = make_case_info env mis LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) in { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } @@ -498,7 +498,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env LetStyle mis in + let ci = make_case_info env mis LetStyle in mkCase (ci, p, cj.uj_val,[|f|] ) in { uj_val = v; uj_type = ccl }) @@ -568,7 +568,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let b2 = f cstrs.(1) b2 in let v = let mis,_ = dest_ind_family indf in - let ci = make_default_case_info env IfStyle mis in + let ci = make_case_info env mis IfStyle in mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in { uj_val = v; uj_type = p } |