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

Ack-by: Zimmi48
Reviewed-by: ppedrot

1 files changed, 6 insertions, 2 deletions

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 *)