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/indfun_common.mli | 7 +++++++
 1 file changed, 7 insertions(+)

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

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e5c756f56..83cadf5f5 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -114,3 +114,10 @@ val acc_rel : Term.constr Util.delayed
 val well_founded : Term.constr Util.delayed
 val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
 val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic
+
+
+                                                        
+type tcc_lemma_value = 
+  | Undefined
+  | Value of Constr.constr
+  | Not_needed
-- 
cgit v1.2.3