Fixes #11231 (missing dependency in pattern-matching decompilation).

The missing dependency impacted the algorithm for detecting default
clauses.

4 files changed, 44 insertions, 2 deletions

diff --git a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst b/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst
new file mode 100644
index 0000000000..ad240ea30b
--- /dev/null
+++ b/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  A dependency was missing when looking for default clauses in the
+  algorithm for printing pattern matching clauses (`#11233
+  <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing
+  `#11231 <https://github.com/coq/coq/pull/11231>`, reported by Barry
+  Jay).
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 862865bd90..037006bc47 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -455,7 +455,9 @@ let rec decomp_branch tags nal flags (avoid,env as e) sigma c =
       (avoid', add_name_opt na' body t env) sigma c
 
 let rec build_tree na isgoal e sigma ci cl =
-  let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in
+  let mkpat n rhs pl =
+    let na = update_name sigma na rhs in
+    na, DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,na) in
   let cnl = ci.ci_pp_info.cstr_tags in
   List.flatten
     (List.init (Array.length cl)
@@ -485,7 +487,9 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
 and contract_branch isgoal e sigma (cdn,mkpat,rhs) =
   let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in
   let mat = align_tree nal isgoal rhs sigma in
-  List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat
+  List.map (fun (ids,hd,rhs) ->
+      let na, pat = mkpat rhs hd in
+      (Nameops.Name.fold_right Id.Set.add na ids, pat, rhs)) mat
 
 (**********************************************************************)
 (* Transform internal representation of pattern-matching into list of *)
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.