diff options
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 60b708f5b..bf166f128 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -183,7 +183,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | _ -> assert false else if dep then - let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in + let realargs = List.rev_map (fun k -> mkRel (i-k)) li in let params = List.map (lift i) vargs in let co = applist (mkConstruct cs.cs_cstr,params@realargs) in Reduction.beta_appvect c [|co|] |