diff options
| author | glondu | 2010-09-28 15:32:01 +0000 |
|---|---|---|
| committer | glondu | 2010-09-28 15:32:01 +0000 |
| commit | 86919192359dee7e274ab4af17bd32efe11a5f44 (patch) | |
| tree | d09d9174894559ce1f34b078e3ae163e9e09515d /pretyping/termops.ml | |
| parent | 013bc34fd828a5eb4eacd721a8021b64abf8a822 (diff) | |
Remove "init" label from Termops.it_mk* specialized functions
These functions are applied much more often without labels than with
them (the alternate of adding the label wherever relevant changes 124
lines instead of 41). Moreover, this is more consistent with the Term
module and there is no ambiguity in argument types. This commit goes
towards elimination of occurrences of OCaml warning 6.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 17e0522230..d31242aa2b 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -235,18 +235,18 @@ let mkProd_wo_LetIn (na,body,t) c = | None -> mkProd (na, t, c) | Some b -> subst1 b c -let it_mkProd ~init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init -let it_mkLambda ~init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init +let it_mkProd init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init +let it_mkLambda init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init let it_named_context_quantifier f ~init = List.fold_left (fun c d -> f d c) init -let it_mkProd_or_LetIn = it_named_context_quantifier mkProd_or_LetIn -let it_mkProd_wo_LetIn = it_named_context_quantifier mkProd_wo_LetIn -let it_mkLambda_or_LetIn = it_named_context_quantifier mkLambda_or_LetIn -let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn -let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_LetIn -let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn +let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init +let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init +let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init +let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init +let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init +let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init (* *) |