diff options
| author | Maxime Dénès | 2017-06-01 15:44:11 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-01 15:44:11 +0200 |
| commit | 84d49e38a245cbbbe5b6111a4e4d9afcbac2d33b (patch) | |
| tree | 0e6bff9cf7c2aaf6967352bd5b5f8c8a2831a570 /pretyping/patternops.ml | |
| parent | 48621da27d52be4825eea271d44bbd7362011dfa (diff) | |
| parent | 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (diff) | |
Merge PR#561: Improving the Name API
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 1c8ad0cddd..0818a55256 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -340,15 +340,15 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) | GLambda (na,bk,c1,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GProd (na,bk,c1,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GLetIn (na,c1,t,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) @@ -411,7 +411,7 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function | { CAst.v = PatVar na } -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; na | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") in |