Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)

Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle

2 files changed, 6 insertions, 5 deletions

diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/closed/bug_3166.v
index baf87631f0..3b3375fdd8 100644
--- a/test-suite/bugs/opened/bug_3166.v
+++ b/test-suite/bugs/closed/bug_3166.v
@@ -80,5 +80,5 @@ Goal forall T (x y : T) (p : x = y), True.
         ) as H0.
   compute in H0.
   change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
-  Fail pose proof (fun k => @eq_trans _ _ _ k H0).
+  pose proof (fun k => @eq_trans _ _ _ k H0).
 Abort.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 984ac4e527..6fd4d37ab4 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -50,10 +50,11 @@ f =
 fun H : B =>
 match H with
 | AC x =>
-    let b0 := b in
-    (if b0 as b return (P b -> True)
-     then fun _ : P true => Logic.I
-     else fun _ : P false => Logic.I) x
+    (fun x0 : P b =>
+     let b0 := b in
+     (if b0 as b return (P b -> True)
+      then fun _ : P true => Logic.I
+      else fun _ : P false => Logic.I) x0) x
 end
      : B -> True
 The command has indeed failed with message: