[ocamlformat] Enable for funind.

As part of the proof refactoring work I am doing some modifications to
`funind` and indentation of that code is driving me a bit crazy; I'd
much prefer to delegate it to an automatic tool.

1 files changed, 87 insertions, 77 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1f2f56ec34..4e0e2dc501 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -15,48 +15,49 @@ open Names
 open Sorts
 open Constr
 open EConstr
-
 open Tacmach.New
 open Tacticals.New
 open Tactics
-
 open Indfun_common
-
 module RelDecl = Context.Rel.Declaration
 
 let is_rec_info sigma scheme_info =
   let test_branche min acc decl =
-    acc || (
-      let new_branche =
-        it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum sigma (RelDecl.get_type decl))) in
-      let free_rels_in_br = Termops.free_rels sigma new_branche in
-      let max = min + scheme_info.Tactics.npredicates in
-      Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br
-    )
+    acc
+    ||
+    let new_branche =
+      it_mkProd_or_LetIn mkProp
+        (fst (decompose_prod_assum sigma (RelDecl.get_type decl)))
+    in
+    let free_rels_in_br = Termops.free_rels sigma new_branche in
+    let max = min + scheme_info.Tactics.npredicates in
+    Int.Set.exists (fun i -> i >= min && i < max) free_rels_in_br
   in
   List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
 
 let choose_dest_or_ind scheme_info args =
   Proofview.tclBIND Proofview.tclEVARMAP (fun sigma ->
-  Tactics.induction_destruct (is_rec_info sigma scheme_info) false args)
+      Tactics.induction_destruct (is_rec_info sigma scheme_info) false args)
 
 let functional_induction with_clean c princl pat =
   let open Proofview.Notations in
   Proofview.Goal.enter_one (fun gl ->
-    let sigma = project gl in
-    let f,args = decompose_app sigma c in
-    match princl with
-    | None -> (* No principle is given let's find the good one *)
-      begin
+      let sigma = project gl in
+      let f, args = decompose_app sigma c in
+      match princl with
+      | None -> (
+        (* No principle is given let's find the good one *)
         match EConstr.kind sigma f with
-        | Const (c',u) ->
+        | Const (c', u) ->
           let princ_option =
-            let finfo = (* we first try to find out a graph on f *)
+            let finfo =
+              (* we first try to find out a graph on f *)
               match find_Function_infos c' with
               | Some finfo -> finfo
               | None ->
-                user_err  (str "Cannot find induction information on "++
-                           Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
+                user_err
+                  ( str "Cannot find induction information on "
+                  ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
             in
             match elimination_sort_of_goal gl with
             | InSProp -> finfo.sprop_lemma
@@ -64,7 +65,8 @@ let functional_induction with_clean c princl pat =
             | InSet -> finfo.rec_lemma
             | InType -> finfo.rect_lemma
           in
-          let sigma, princ =  (* then we get the principle *)
+          let sigma, princ =
+            (* then we get the principle *)
             match princ_option with
             | Some princ ->
               Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ)
@@ -79,66 +81,74 @@ let functional_induction with_clean c princl pat =
               in
               let princ_ref =
                 try
-                  Constrintern.locate_reference (Libnames.qualid_of_ident princ_name)
-                with
-                | Not_found ->
-                  user_err (str "Cannot find induction principle for "
-                            ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
+                  Constrintern.locate_reference
+                    (Libnames.qualid_of_ident princ_name)
+                with Not_found ->
+                  user_err
+                    ( str "Cannot find induction principle for "
+                    ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
               in
               Evd.fresh_global (pf_env gl) (project gl) princ_ref
           in
           let princt = Retyping.get_type_of (pf_env gl) sigma princ in
-          Proofview.Unsafe.tclEVARS sigma <*>
-          Proofview.tclUNIT (princ, Tactypes.NoBindings, princt, args)
+          Proofview.Unsafe.tclEVARS sigma
+          <*> Proofview.tclUNIT (princ, Tactypes.NoBindings, princt, args)
         | _ ->
-          CErrors.user_err (str "functional induction must be used with a function" )
-      end
-    | Some ((princ,binding)) ->
-      let sigma, princt = pf_type_of gl princ in
-      Proofview.Unsafe.tclEVARS sigma <*>
-      Proofview.tclUNIT (princ, binding, princt, args)
-    ) >>= fun (princ, bindings, princ_type, args) ->
+          CErrors.user_err
+            (str "functional induction must be used with a function") )
+      | Some (princ, binding) ->
+        let sigma, princt = pf_type_of gl princ in
+        Proofview.Unsafe.tclEVARS sigma
+        <*> Proofview.tclUNIT (princ, binding, princt, args))
+  >>= fun (princ, bindings, princ_type, args) ->
   Proofview.Goal.enter (fun gl ->
-  let sigma = project gl in
-  let princ_infos = compute_elim_sig (project gl) princ_type in
-  let args_as_induction_constr =
-    let c_list =
-      if princ_infos.Tactics.farg_in_concl
-      then [c] else []
-    in
-    if List.length args + List.length c_list = 0
-    then user_err Pp.(str "Cannot recognize a valid functional scheme" );
-    let encoded_pat_as_patlist =
-      List.make (List.length args + List.length c_list - 1) None @ [pat]
-    in
-    List.map2
-      (fun c pat ->
-         ((None, ElimOnConstr (fun env sigma -> (sigma,(c,Tactypes.NoBindings)))),
-          (None,pat), None))
-      (args@c_list)
-      encoded_pat_as_patlist
-  in
-  let princ' = Some (princ,bindings) in
-  let princ_vars =
-    List.fold_right
-      (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
-      args
-      Id.Set.empty
-  in
-  let old_idl = List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty in
-  let old_idl = Id.Set.diff old_idl princ_vars in
-  let subst_and_reduce gl =
-    if with_clean
-    then
-      let idl = List.filter (fun id -> not (Id.Set.mem id old_idl))(pf_ids_of_hyps gl) in
-      let flag = Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false } in
+      let sigma = project gl in
+      let princ_infos = compute_elim_sig (project gl) princ_type in
+      let args_as_induction_constr =
+        let c_list = if princ_infos.Tactics.farg_in_concl then [c] else [] in
+        if List.length args + List.length c_list = 0 then
+          user_err Pp.(str "Cannot recognize a valid functional scheme");
+        let encoded_pat_as_patlist =
+          List.make (List.length args + List.length c_list - 1) None @ [pat]
+        in
+        List.map2
+          (fun c pat ->
+            ( ( None
+              , ElimOnConstr
+                  (fun env sigma -> (sigma, (c, Tactypes.NoBindings))) )
+            , (None, pat)
+            , None ))
+          (args @ c_list) encoded_pat_as_patlist
+      in
+      let princ' = Some (princ, bindings) in
+      let princ_vars =
+        List.fold_right
+          (fun a acc ->
+            try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
+          args Id.Set.empty
+      in
+      let old_idl =
+        List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty
+      in
+      let old_idl = Id.Set.diff old_idl princ_vars in
+      let subst_and_reduce gl =
+        if with_clean then
+          let idl =
+            List.filter
+              (fun id -> not (Id.Set.mem id old_idl))
+              (pf_ids_of_hyps gl)
+          in
+          let flag =
+            Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false}
+          in
+          tclTHEN
+            (tclMAP
+               (fun id ->
+                 tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id]))
+               idl)
+            (reduce flag Locusops.allHypsAndConcl)
+        else tclIDTAC
+      in
       tclTHEN
-        (tclMAP (fun id -> tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl)
-        (reduce flag Locusops.allHypsAndConcl)
-    else tclIDTAC
-  in
-  tclTHEN
-    (choose_dest_or_ind
-       princ_infos
-       (args_as_induction_constr,princ'))
-    (Proofview.Goal.enter subst_and_reduce))
+        (choose_dest_or_ind princ_infos (args_as_induction_constr, princ'))
+        (Proofview.Goal.enter subst_and_reduce))