From 46a8fe0ef1c06ff1b64082ff87b8725dbbd4989b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 5 Dec 2018 01:50:37 +0100
Subject: [plugins] [funind] Adapt to removal of imperative proof state.

---
 plugins/funind/recdef.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 549f1fc0e4..a006c2c354 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -14,6 +14,6 @@ bool ->
            int -> Constrexpr.constr_expr -> (pconstant ->
             Indfun_common.tcc_lemma_value ref ->
             pconstant ->
-            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit
+            pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option
 
 
-- 
cgit v1.2.3