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.ml | 6 ++++++
 1 file changed, 6 insertions(+)

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

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f56e92414..8419f1d8f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -506,3 +506,9 @@ let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
     (List.fold_right
        (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
+
+                                                          
+type tcc_lemma_value = 
+  | Undefined
+  | Value of Constr.constr
+  | Not_needed
-- 
cgit v1.2.3