Merge PR #11776: [ocamlformat] Enable for funind.

Reviewed-by: Matafou
Ack-by: Zimmi48
Ack-by: maximedenes

1 files changed, 20 insertions, 12 deletions

diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 64fbfaeedf..52089ca7fb 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,19 +1,27 @@
 open Names
 
 val prove_princ_for_struct :
-  Evd.evar_map ref ->
-  bool ->
-  int -> Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic
-
+     Evd.evar_map ref
+  -> bool
+  -> int
+  -> Constant.t array
+  -> EConstr.constr array
+  -> int
+  -> Tacmach.tactic
 
 val prove_principle_for_gen :
-  Constant.t * Constant.t * Constant.t -> (* name of the function, the functional and the fixpoint equation *)
-  Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *)
-  bool -> (* is that function uses measure *)
-  int -> (* the number of recursive argument *)
-  EConstr.types -> (* the type of the recursive argument *)
-  EConstr.constr -> (* the wf relation used to prove the function *)
-  Tacmach.tactic
-
+     Constant.t * Constant.t * Constant.t
+  -> (* name of the function, the functional and the fixpoint equation *)
+     Indfun_common.tcc_lemma_value ref
+  -> (* a pointer to the obligation proofs lemma *)
+     bool
+  -> (* is that function uses measure *)
+     int
+  -> (* the number of recursive argument *)
+     EConstr.types
+  -> (* the type of the recursive argument *)
+     EConstr.constr
+  -> (* the wf relation used to prove the function *)
+     Tacmach.tactic
 
 (* val is_pte  : rel_declaration -> bool  *)