diff options
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 5e771245c9..7a43c44f9b 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) |