From aedf2c0044b04cf141a52b1398306111b0bc4321 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 8 Mar 2020 01:23:02 -0500
Subject: [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.
---
 plugins/funind/functional_principles_proofs.mli | 32 +++++++++++++++----------
 1 file changed, 20 insertions(+), 12 deletions(-)

(limited to 'plugins/funind/functional_principles_proofs.mli')

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  *)
-- 
cgit v1.2.3