diff options
| author | letouzey | 2013-02-18 15:42:36 +0000 |
|---|---|---|
| committer | letouzey | 2013-02-18 15:42:36 +0000 |
| commit | ddc9c1bd8e1eaae186468f093e467d8f2e1091cd (patch) | |
| tree | 6543bbcdca657cfd315be224531f66fed5adb280 /pretyping | |
| parent | 648c594489f8d0ffdde9596b87f5c1ff6ccef612 (diff) | |
use List.rev_map whenever possible
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 60e3025b46..2910774db6 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2135,7 +2135,7 @@ let abstract_tomatch env tomatchs tycon = let build_dependent_signature env evars avoid tomatchs arsign = let avoid = ref avoid in let arsign = List.rev arsign in - let allnames = List.rev (List.map (List.map pi1) arsign) in + let allnames = List.rev_map (List.map pi1) arsign in let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in let eqs, neqs, refls, slift, arsign' = List.fold_left2 diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 60b708f5b1..bf166f1286 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|] diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 777e6c1d80..cc6ec1e95e 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -225,7 +225,7 @@ let compute_canonical_projections (con,ind) = let v = mkConst con in let c = Environ.constant_value (Global.env()) con in let lt,t = Reductionops.splay_lam (Global.env()) Evd.empty c in - let lt = List.rev (List.map snd lt) in + let lt = List.rev_map snd lt in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in |