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

Ack-by: Zimmi48
Reviewed-by: ppedrot

5 files changed, 47 insertions, 4 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..941469d698
--- /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/printing/ppconstr.ml b/printing/ppconstr.ml
index 2da163b8ee..b55a41471a 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -275,7 +275,7 @@ let tag_var = tag Tag.variable
         pr_reference r, latom
 
       | CPatOr pl ->
-        let pp = pr_patt mt (lpator,Any) in
+        let pp p = hov 0 (pr_patt mt (lpator,Any) p) in
         surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator
 
       | CPatNotation ((_,"( _ )"),([p],[]),[]) ->
@@ -304,7 +304,8 @@ let tag_var = tag Tag.variable
     spc() ++ hov 4
       (pr_with_comments ?loc
          (str "| " ++
-            hov 0 (prlist_with_sep pr_spcbar (prlist_with_sep sep_v (pr_patt ltop)) pl
+            hov 0 (prlist_with_sep pr_spcbar
+                     (fun p -> hov 0 (prlist_with_sep sep_v (pr_patt ltop) p)) pl
                    ++ str " =>") ++
             pr_sep_com spc (pr ltop) rhs))
 
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.