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, 17 insertions, 19 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4f96ce06e0..bc12fcea9c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
   let coq_I = Coqlib.build_coq_I () in
   let rec scan_type  context type_of_hyp : tactic =
     if isLetIn type_of_hyp then
-      let real_type_of_hyp = it_mkProd_or_LetIn ~init:type_of_hyp context in
+      let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
       let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
       (* length of context didn't change ? *)
       let new_context,new_typ_of_hyp =
@@ -406,13 +406,13 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
     then
       begin
 	let (x,t_x,t') = destProd type_of_hyp in
-	let actual_real_type_of_hyp = it_mkProd_or_LetIn ~init:t' context in
+	let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in
 	if is_property ptes_infos t_x actual_real_type_of_hyp then
 	  begin
 	    let pte,pte_args =  (destApp t_x) in
 	    let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in
 	    let popped_t' = pop t' in
-	    let real_type_of_hyp = it_mkProd_or_LetIn ~init:popped_t' context in
+	    let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in
 	    let prove_new_type_of_hyp =
 	      let context_length = List.length context in
 	      tclTHENLIST
@@ -463,7 +463,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 (* 		    );  *)
 	  let popped_t' = pop t' in
 	  let real_type_of_hyp =
-	    it_mkProd_or_LetIn ~init:popped_t' context
+	    it_mkProd_or_LetIn popped_t' context
 	  in
 	  let prove_trivial =
 	    let nb_intro = List.length context in
@@ -491,7 +491,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	then (*  t_x :=  t = t   => we remove this precond *)
 	  let popped_t' = pop t' in
 	  let real_type_of_hyp =
-	    it_mkProd_or_LetIn ~init:popped_t' context
+	    it_mkProd_or_LetIn popped_t' context
 	  in
 	  let hd,args = destApp t_x in
 	  let get_args hd args =
@@ -954,7 +954,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args)
     (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
-  let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in
+  let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
   let f_id = id_of_label (con_label (destConst f)) in
   let prove_replacement =
     tclTHENSEQ
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 5ac5f9ce84..e0b08599d0 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -114,9 +114,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   let pre_princ =
     it_mkProd_or_LetIn
-      ~init:
       (it_mkProd_or_LetIn
-	 ~init:(Option.fold_right
+	 (Option.fold_right
 			   mkProd_or_LetIn
 			   princ_type_info.indarg
 			   princ_type_info.concl
@@ -267,10 +266,10 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       (lift (List.length ptes_vars) pre_res)
   in
   it_mkProd_or_LetIn
-    ~init:(it_mkProd_or_LetIn
-	     ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b)
-			      new_predicates)
-	  )
+    (it_mkProd_or_LetIn
+       pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b)
+          	      new_predicates)
+    )
     princ_type_info.params
 
 
@@ -291,8 +290,7 @@ let change_property_sort toSort princ princName =
 	    (fun i -> mkRel (nargs - i )))
   in
   it_mkLambda_or_LetIn
-    ~init:
-    (it_mkLambda_or_LetIn ~init
+    (it_mkLambda_or_LetIn init
        (List.map change_sort_in_predicate princ_info.predicates)
     )
     princ_info.params
@@ -639,7 +637,7 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
 	     const
 	 with Found_type i ->
 	   let princ_body =
-	     Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt
+	     Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
 	   in
 	   {const with
 	      Entries.const_entry_body = princ_body;
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 90d7baeef4..f0ea133c60 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -248,7 +248,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	     | [] | [_] | [_;_] -> anomaly "bad context"
 	     | hres::res::(x,_,t)::ctxt ->
 		 Termops.it_mkLambda_or_LetIn
-		   ~init:(Termops.it_mkProd_or_LetIn ~init:concl [hres;res])
+		   (Termops.it_mkProd_or_LetIn concl [hres;res])
 		   ((x,None,t)::ctxt)
 	)
 	lemmas_types_infos
@@ -627,7 +627,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     *)
     let lemmas =
       Array.map
-	(fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn ~init:concl ctxt))
+	(fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn concl ctxt))
 	lemmas_types_infos
     in
     (* We get the constant and the principle corresponding to this lemma *)
@@ -754,7 +754,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
 	     generate_type false const_of_f graph i
 	   in
-	   let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in
+	   let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
 	   let type_of_lemma = nf_zeta type_of_lemma in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
 	   type_of_lemma,type_info
@@ -809,7 +809,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   let (type_of_lemma_ctxt,type_of_lemma_concl) as type_info =
 	     generate_type true  const_of_f graph i
 	   in
-	   let type_of_lemma = Termops.it_mkProd_or_LetIn ~init:type_of_lemma_concl type_of_lemma_ctxt in
+	   let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
 	   let type_of_lemma = nf_zeta type_of_lemma in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
 	   type_of_lemma,type_info