From c7dd03f804fabde7b201677058b8e1b9c62a7793 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 18 Aug 2017 01:03:22 +0200 Subject: Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map (from module List). --- pretyping/cases.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/cases.ml') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 49f073d66..fe5b90e04 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1753,14 +1753,14 @@ let build_inversion_problem loc env sigma tms t = let cstr,u = destConstruct sigma f in let n = constructor_nrealargs_env env cstr in let l = List.lastn n (Array.to_list v) in - let l,acc = List.fold_map' reveal_pattern l acc in + let l,acc = List.fold_right_map reveal_pattern l acc in CAst.make (PatCstr (cstr,l,Anonymous)), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with | [] -> [], acc_sign, acc | (t, IsInd (_,IndType(indf,realargs),_)) :: tms -> - let patl,acc = List.fold_map' reveal_pattern realargs acc in + let patl,acc = List.fold_right_map reveal_pattern realargs acc in let pat,acc = make_patvar t acc in let indf' = lift_inductive_family n indf in let sign = make_arity_signature env sigma true indf' in -- cgit v1.2.3