diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-16 13:22:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | be83b52cf50ed4c596e40cfd52da03258a7a4a18 (patch) | |
| tree | 92e1e62378d2274751ab46673e2ee56fe4f65999 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/glob_term.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/glob_term.mli b/intf/glob_term.mli index 5e771245c..7a43c44f9 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -67,7 +67,7 @@ and fix_kind = | GCoFix of int and predicate_pattern = - Name.t * (Loc.t * inductive * Name.t list) option + Name.t * (inductive * Name.t list) Loc.located option (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) and tomatch_tuple = (glob_constr * predicate_pattern) |