diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a7e73c91f..ae7364052 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -96,7 +96,7 @@ open Decl_kinds let pr_set_entry_type = function | ETName -> str"ident" | ETReference -> str"global" - | ETPattern -> str"pattern" + | ETPattern _ -> str"pattern" | ETConstr _ -> str"constr" | ETOther (_,e) -> str e | ETBigint -> str "bigint" |