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

3 files changed, 18 insertions, 18 deletions

diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index e7c9331527..c3c6b205d9 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -131,9 +131,9 @@ let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
 let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
 
 let it_mkProd_or_LetIn_name env b hyps =
-  it_mkProd_or_LetIn ~init:b (name_context env hyps)
+  it_mkProd_or_LetIn b (name_context env hyps)
 let it_mkLambda_or_LetIn_name env b hyps =
-  it_mkLambda_or_LetIn ~init:b (name_context env hyps)
+  it_mkLambda_or_LetIn b (name_context env hyps)
 
 (**********************************************************************)
 (* Fresh names *)
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
 
 (* *)
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 1346a7f524..385bd3022a 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -49,14 +49,14 @@ val extended_rel_vect : int -> rel_context -> constr array
 (** iterators/destructors on terms *)
 val mkProd_or_LetIn : rel_declaration -> types -> types
 val mkProd_wo_LetIn : rel_declaration -> types -> types
-val it_mkProd : init:types -> (name * types) list -> types
-val it_mkLambda : init:constr -> (name * types) list -> constr
-val it_mkProd_or_LetIn   : init:types -> rel_context -> types
-val it_mkProd_wo_LetIn : init:types -> rel_context -> types
-val it_mkLambda_or_LetIn : init:constr -> rel_context -> constr
-val it_mkNamedProd_or_LetIn   : init:types -> named_context -> types
-val it_mkNamedProd_wo_LetIn   : init:types -> named_context -> types
-val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr
+val it_mkProd : types -> (name * types) list -> types
+val it_mkLambda : constr -> (name * types) list -> constr
+val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkProd_wo_LetIn : types -> rel_context -> types
+val it_mkLambda_or_LetIn : constr -> rel_context -> constr
+val it_mkNamedProd_or_LetIn : types -> named_context -> types
+val it_mkNamedProd_wo_LetIn : types -> named_context -> types
+val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
 
 val it_named_context_quantifier :
   (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a