diff options
| author | Emilio Jesus Gallego Arias | 2017-01-16 13:22:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-24 23:58:23 +0200 |
| commit | be83b52cf50ed4c596e40cfd52da03258a7a4a18 (patch) | |
| tree | 92e1e62378d2274751ab46673e2ee56fe4f65999 /pretyping/patternops.ml | |
| parent | ad3aab9415b98a247a6cbce05752632c3c42391c (diff) | |
[location] Move Glob_term.predicate_pattern to located.
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 8c570dffee..48ae93f3ef 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -380,13 +380,13 @@ let rec pat_of_raw metas vars = function | _ -> None in let ind_tags,ind = match indnames with - | Some (_,ind,nal) -> Some (List.length nal), Some ind + | Some (_,(ind,nal)) -> Some (List.length nal), Some ind | None -> None, get_ind brs in let ext,brs = pats_of_glob_branches loc metas vars ind brs in let pred = match p,indnames with - | Some p, Some (_,_,nal) -> + | Some p, Some (_,(_,nal)) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) | (None | Some (GHole _)), _ -> PMeta None |