diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 35ef1e620f..0a3e28c6cd 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1014,7 +1014,7 @@ let interp c = match c with | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacOpenScope sc -> vernac_open_scope sc | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl - | VernacInfix (assoc,n,inf,qid,sc) -> vernac_infix assoc n inf qid sc + | VernacInfix (assoc,n,inf,qid,b,sc) -> vernac_infix assoc n inf qid b sc | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc | VernacNotation (inf,c,pl,sc) -> vernac_notation inf c pl sc |