diff options
| author | Gaëtan Gilbert | 2019-02-21 13:12:50 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-28 14:27:59 +0100 |
| commit | 5a760abecb8ef8a1feea9fbfd33c33f96519c0ba (patch) | |
| tree | a9dd62b33a6b9143920ff17b87dd10ef238a58dc | |
| parent | 53bafd5df5b025d8b168cb73a8bb44115ca504fa (diff) | |
Print location for type error in pattern variable
See #9616
| -rw-r--r-- | pretyping/cases.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ed7c3d6770..1ad90b2953 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -426,7 +426,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in (match find_row_ind tm1 with | None -> sigma, (current, tmtyp) - | Some (_,(ind,_)) -> + | Some (loc,(ind,_)) -> let sigma, indt = inductive_template !!(pb.env) sigma None ind in let sigma, current = if List.is_empty deps && isEvar sigma typ then @@ -435,7 +435,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = | None -> sigma, current | Some sigma -> sigma, current else - let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in + let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val in sigma, (current, try_find_ind !!(pb.env) sigma indt names)) |