diff options
author | 2017-01-16 13:22:42 +0100 | |
---|---|---|
committer | 2017-04-24 23:58:23 +0200 | |
commit | be83b52cf50ed4c596e40cfd52da03258a7a4a18 (patch) | |
tree | 92e1e62378d2274751ab46673e2ee56fe4f65999 /plugins/syntax/ascii_syntax.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 'plugins/syntax/ascii_syntax.ml')
0 files changed, 0 insertions, 0 deletions