Merge PR#538: Correction of bug #4306

7 files changed, 58 insertions, 12 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0bbe4bb4c..a380443fe 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -291,7 +291,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	 Can be safely replaced by the next comment for Ocaml >= 3.08.4
       *)
       let sub = Int.Map.bindings sub in
-      List.fold_left (fun end_of_type (i,t)  -> lift 1 (substnl  [t] (i-1) end_of_type))
+      List.fold_left (fun end_of_type (i,t)  -> liftn 1 i (substnl  [t] (i-1) end_of_type))
 	end_of_type_with_pop
 	sub
     in
@@ -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_I ()
   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
 
diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v
new file mode 100644
index 000000000..4aef5bb95
--- /dev/null
+++ b/test-suite/bugs/closed/4306.v
@@ -0,0 +1,32 @@
+Require Import List.
+Require Import Arith.
+Require Import Recdef. 
+Require Import Omega.
+
+Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
+  match xys with
+    | (nil, _) => snd xys
+    | (_, nil) => fst xys
+    | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+                                | Lt => x :: foo (xs', y :: ys')
+                                | Eq => x :: foo (xs', ys')
+                                | Gt => y :: foo (x :: xs', ys')
+                              end
+  end.
+Proof.
+  intros; simpl; omega.
+  intros; simpl; omega.
+  intros; simpl; omega.
+Qed.
+
+Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
+  let (xs, ys) := xys in
+  match (xs, ys) with
+    | (nil, _) => ys
+    | (_, nil) => xs
+    | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+                                | Lt => x :: foo (xs', ys)
+                                | Eq => x :: foo (xs', ys')
+                                | Gt => y :: foo (xs, ys')
+                              end
+  end.
\ No newline at end of file