diff options
Diffstat (limited to 'contrib/subtac/equations.ml4')
| -rw-r--r-- | contrib/subtac/equations.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4 index 135fcf11dc..ebbb5505f6 100644 --- a/contrib/subtac/equations.ml4 +++ b/contrib/subtac/equations.ml4 @@ -850,7 +850,7 @@ let ids_of_patc c ?(bound=Idset.empty) l = in let rec aux bdvars l c = match c with | CRef (Ident lid) -> found lid bdvars l - | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) -> + | CNotation (_, "{ _ : _ | _ }", ((CRef (Ident (_, id))) :: _,[])) when not (Idset.mem id bdvars) -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c in aux bound l c |