aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cases.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-18 01:03:22 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-29 05:10:40 +0200
commitc7dd03f804fabde7b201677058b8e1b9c62a7793 (patch)
treec9029c8fbba22296615b1311d802a68d31526b0a /pretyping/cases.ml
parent2ad320f630e138fc608af836a744a4704be42558 (diff)
Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map
(from module List).
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r--pretyping/cases.ml4
1 files changed, 2 insertions, 2 deletions
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