Merge PR #13694: Add a test for a complex conversion involving pattern-matching with let-bindings

Reviewed-by: SkySkimmer

2 files changed, 54 insertions, 0 deletions

diff --git a/test-suite/success/case_let_conversion.v b/test-suite/success/case_let_conversion.v
new file mode 100644
index 0000000000..3f1ab96fe1
--- /dev/null
+++ b/test-suite/success/case_let_conversion.v
@@ -0,0 +1,39 @@
+Axiom checker_flags : Set.
+
+Inductive Box (R : Type) : Type := box : Box R.
+
+Inductive typing (H : checker_flags) : Type :=
+| type_Rel : typing H -> typing H
+| type_Case : let i := tt in Box (typing H) -> typing H.
+
+Definition unbox (P : Type) (b : Box P) := match b with box _ => 0 end.
+
+Definition size (H : checker_flags) (d : typing H) : nat.
+Proof.
+revert d.
+fix size 1.
+destruct 1.
+- exact (size d).
+- exact (unbox _ b).
+Defined.
+
+Definition foo (H : checker_flags) (a : typing H) :
+  size H (type_Rel H a) = size H a.
+Proof.
+simpl.
+reflexivity.
+Qed.
+
+Definition bar (H : checker_flags) (a : typing H) :
+  size H (type_Rel H a) = size H a.
+Proof.
+vm_compute.
+reflexivity.
+Qed.
+
+Definition qux (H : checker_flags) (a : typing H) :
+  size H (type_Rel H a) = size H a.
+Proof.
+native_compute.
+reflexivity.
+Qed.
diff --git a/test-suite/success/case_let_param.v b/test-suite/success/case_let_param.v
new file mode 100644
index 0000000000..46d8c26e83
--- /dev/null
+++ b/test-suite/success/case_let_param.v
@@ -0,0 +1,15 @@
+Inductive foo (x := tt) := Foo : forall (y := x), foo.
+
+Definition get (t : foo) := match t with Foo _ y => y end.
+
+Goal get Foo = tt.
+Proof.
+reflexivity.
+Qed.
+
+Goal forall x : foo,
+  match x with Foo _ y => y end = match x with Foo _ _ => tt end.
+Proof.
+intros.
+reflexivity.
+Qed.