Merge PR #11233: Fixes #11231: missing dependency in looking for default clauses in pattern matching decompilation algorithm

Ack-by: Zimmi48
Reviewed-by: ppedrot

2 files changed, 32 insertions, 0 deletions

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index e84ac85aa8..6976610b22 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -166,3 +166,15 @@ fun x : K => match x with
      : K -> nat
 The command has indeed failed with message:
 Pattern "S _, _" is redundant in this clause.
+stray = 
+fun N : Tree =>
+match N with
+| App (App Node (Node as strayvariable)) _ |
+  App (App Node (App Node _ as strayvariable)) _ |
+  App (App Node (App (App Node Node) (App _ _) as strayvariable)) _ |
+  App (App Node (App (App Node (App _ _)) _ as strayvariable)) _ |
+  App (App Node (App (App (App _ _) _) _ as strayvariable)) _ =>
+    strayvariable
+| _ => Node
+end
+     : Tree -> Tree
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index a040b69b44..262ec2b677 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -222,3 +222,23 @@ Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end.
 
 (* Test redundant clause within a disjunctive pattern *)
 Fail Check fun n m => match n, m with 0, 0 | _, S _ | S 0, _ | S (S _ | _), _ => false end.
+
+Module Bug11231.
+
+(* Missing dependency in computing if a clause is a default clause *)
+
+Inductive Tree: Set :=
+| Node : Tree
+| App : Tree -> Tree -> Tree
+.
+
+Definition stray N :=
+match N with
+| App (App Node (App (App Node Node) Node)) _ => Node
+| App (App Node strayvariable) _ => strayvariable
+| _ => Node
+end.
+
+Print stray.
+
+End Bug11231.