diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aa6ec1c941..29d6726262 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -436,7 +436,7 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = | exception Evarconv.UnableToUnify _ -> sigma, current | sigma -> sigma, current else - let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in + let sigma, j, _trace = 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)) @@ -1955,8 +1955,12 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon = match tycon with - | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma - ~flags:(default_flags_of TransparentState.full) j p + | Some p -> + let (evd,v,_trace) = + Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma + ~flags:(default_flags_of TransparentState.full) j p + in + (evd,v) | None -> sigma, j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) @@ -2160,7 +2164,7 @@ let constr_of_pat env sigma arsign pat avoid = let IndType (indf, _) = try find_rectype env sigma (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env sigma - {uj_val = ty; uj_type = Typing.unsafe_type_of env sigma ty} + {uj_val = ty; uj_type = Retyping.get_type_of env sigma ty} in let (ind,u), params = dest_ind_family indf in let params = List.map EConstr.of_constr params in |