From 043c3907f9ed23ae9b9642d2cbb651f6a29737bd Mon Sep 17 00:00:00 2001
From: Julien Forest <forest@ensiie.fr>
Date: Fri, 31 Mar 2017 19:48:03 +0200
Subject: Solving first problem in bug #4306. TO DO : solve the let in problem

---
 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 f60eedbe6..c84c736b8 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -13,7 +13,7 @@ bool ->
            Constrexpr.constr_expr ->
            Constrexpr.constr_expr ->
            int -> Constrexpr.constr_expr -> (Term.pconstant ->
-            Term.constr option ref ->
+            Indfun_common.tcc_lemma_value ref ->
             Term.pconstant ->
             Term.pconstant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit
 
-- 
cgit v1.2.3