Solving first problem in bug #4306. TO DO : solve the let in problem

6 files changed, 25 insertions, 11 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0bbe4bb4c..85084badd 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1388,8 +1388,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 
 let prove_with_tcc tcc_lemma_constr eqs : tactic =
   match !tcc_lemma_constr with
-    | None -> anomaly (Pp.str "No tcc proof !!")
-    | Some lemma ->
+  | Undefined -> anomaly (Pp.str "No tcc proof !!")
+  | Value lemma ->
 	fun gls ->
 (* 	  let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
 (* 	  let ids = hid::pf_ids_of_hyps gls in  *)
@@ -1407,7 +1407,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 	      Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some []))
 	    ]
 	    gls
-
+  | Not_needed -> tclIDTAC
 
 let backtrack_eqs_until_hrec hrec eqs : tactic =
   fun gls ->
@@ -1586,8 +1586,9 @@ let prove_principle_for_gen
   let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
-     | None -> error "No tcc proof !!"
-     | Some lemma -> lemma
+     | Undefined -> error "No tcc proof !!"
+     | Value lemma -> lemma
+     | Not_needed -> Coqlib.build_coq_True ()
   in
 (*   let rec list_diff del_list check_list = *)
 (*     match del_list with *)
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 34ce66967..e11cd9eac 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -9,7 +9,7 @@ val prove_princ_for_struct :
 
 val prove_principle_for_gen :
   constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *)
-  constr option ref -> (* a pointer to the obligation proofs lemma *)
+  Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *)
   bool -> (* is that function uses measure *)
   int -> (* the number of recursive argument *)
   types -> (* the type of the recursive argument *)
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
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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index fa84e4ddf..7ff31f112 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -41,7 +41,7 @@ open Eauto
 open Indfun_common
 open Sigma.Notations
 open Context.Rel.Declaration
-
+       
 
 (* Ugly things which should not be here *)
 
@@ -1296,7 +1296,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
     in
     let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
-    ref_ := Some lemma ;
+    ref_ := Value lemma ;
     let lid = ref [] in
     let h_num = ref (-1) in
     let env = Global.env () in
@@ -1412,6 +1412,7 @@ let com_terminate
       (new_goal_type);
   with Failure "empty list of subgoals!" ->
     (* a non recursive function declared with measure ! *)
+    tcc_lemma_ref := Not_needed;
     defined ()
 
 
@@ -1484,7 +1485,6 @@ let (com_eqn : int -> Id.t ->
 (*      Pp.msgnl (str "eqn finished"); *)
     );;
 
-
 let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
     generate_induction_principle using_lemmas : unit =
   let env = Global.env() in
@@ -1524,7 +1524,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   in
   let evm = Evd.from_ctx evuctx in
   let tcc_lemma_name = add_suffix function_name "_tcc" in
-  let tcc_lemma_constr = ref None in
+  let tcc_lemma_constr = ref Undefined in
   (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook _ _ = 
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
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