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.

1 files changed, 32 insertions, 0 deletions

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