Merge branch v8.6 into trunk

Note: I removed what seemed to be dead code in recdef.ml (local_assum
and local_def introduced with econstr branch), assuming that this is
what should be done.

7 files changed, 55 insertions, 18 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 48c0f5f04..8dae17d69 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -299,7 +299,7 @@ let change_eq env sigma hyp_id (context:rel_context) 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
@@ -1401,8 +1401,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  *)
@@ -1420,7 +1420,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 ->
@@ -1599,8 +1599,9 @@ let prove_principle_for_gen
   let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
-     | None -> error "No tcc proof !!"
-     | Some lemma -> EConstr.of_constr lemma
+     | Undefined -> error "No tcc proof !!"
+     | Value lemma -> EConstr.of_constr lemma
+     | Not_needed -> EConstr.of_constr (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 769d726d7..7ddc84d01 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 *)
   EConstr.types -> (* the type of the recursive argument *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 20da12f39..7b0d7d27d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -543,3 +543,8 @@ let prodn n env b =
 
 (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
 let compose_prod l b = prodn (List.length l) l b
+
+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 5c3e73e9d..5ef8f05bb 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -119,3 +119,8 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
   (Names.Name.t * EConstr.t) list * EConstr.t
 val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
 val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
+                                                        
+type tcc_lemma_value = 
+  | Undefined
+  | Value of Constr.constr
+  | Not_needed
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5460d6fb7..26ba5ef40 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -45,12 +45,6 @@ open Indfun_common
 open Sigma.Notations
 open Context.Rel.Declaration
 
-let local_assum (na, t) =
-  LocalAssum (na, EConstr.Unsafe.to_constr t)
-
-let local_def (na, b, t) =
-  LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
-
 (* Ugly things which should not be here *)
 
 let coq_constant m s =
@@ -1323,7 +1317,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 (EConstr.Unsafe.to_constr lemma);
+    ref_ := Value (EConstr.Unsafe.to_constr lemma);
     let lid = ref [] in
     let h_num = ref (-1) in
     let env = Global.env () in
@@ -1411,7 +1405,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 
 let com_terminate
     tcc_lemma_name
-    (tcc_lemma_ref : Constr.t option ref)
+    tcc_lemma_ref
     is_mes
     fonctional_ref
     input_type
@@ -1440,6 +1434,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 ()
 
 
@@ -1515,7 +1510,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 open Term in
@@ -1561,7 +1555,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 9c1081b9d..80f02e01c 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 -> EConstr.types -> int -> EConstr.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