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/recdef.mli | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

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

diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 3225411c85..4e5146e37c 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,13 +1,13 @@
 open Constr
 
-val tclUSER_if_not_mes
-  : unit Proofview.tactic
+val tclUSER_if_not_mes :
+     unit Proofview.tactic
   -> bool
   -> Names.Id.t list option
   -> unit Proofview.tactic
 
-val recursive_definition
-  :  interactive_proof:bool
+val recursive_definition :
+     interactive_proof:bool
   -> is_mes:bool
   -> Names.Id.t
   -> Constrintern.internalization_env
@@ -15,7 +15,14 @@ val recursive_definition
   -> Constrexpr.constr_expr
   -> int
   -> Constrexpr.constr_expr
-  -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant ->
-      pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit)
+  -> (   pconstant
+      -> Indfun_common.tcc_lemma_value ref
+      -> pconstant
+      -> pconstant
+      -> int
+      -> EConstr.types
+      -> int
+      -> EConstr.constr
+      -> unit)
   -> Constrexpr.constr_expr list
   -> Lemmas.t option
-- 
cgit v1.2.3