diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-10 19:38:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-12 13:30:58 +0100 |
| commit | dd47b90184440eacafac0d98bbd3b24b57579df1 (patch) | |
| tree | 07809d153bccb5ec51913d4f320d6283234ebe70 /pretyping/detyping.ml | |
| parent | 5c9d569cee804c099c44286777ab084e0370399f (diff) | |
Decompiling pattern-matching: mini-removal dead code.
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 5906d5878..23993243f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -367,10 +367,9 @@ let rec decomp_branch tags nal b (avoid,env as e) 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 cnl = ci.ci_pp_info.cstr_tags in - let cna = ci.ci_cstr_nargs in List.flatten (List.init (Array.length cl) - (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i)))) + (fun i -> contract_branch isgoal e sigma (cnl.(i),mkpat i,cl.(i)))) and align_tree nal isgoal (e,c as rhs) sigma = match nal with | [] -> [Id.Set.empty,[],rhs] @@ -390,10 +389,10 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with | _ -> let na = update_name sigma na rhs in let pat = DAst.make @@ PatVar na in - let mat = align_tree nal isgoal rhs sigma in + let mat = align_tree nal isgoal rhs sigma in List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat -and contract_branch isgoal e sigma (cdn,can,mkpat,rhs) = +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 |