diff options
Diffstat (limited to 'pretyping/glob_term.mli')
| -rw-r--r-- | pretyping/glob_term.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index f13d0bee9..a4feac358 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -82,9 +82,8 @@ and fix_kind = | GCoFix of int and predicate_pattern = - name * (loc * inductive * int * name list) option - (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)], [k] - is the number of parameter of [I]. *) + name * (loc * inductive * name list) option + (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) and tomatch_tuple = (glob_constr * predicate_pattern) |