diff options
| author | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
| commit | dd84c113a154742dff86328ebc758097e9aac8eb (patch) | |
| tree | 67795fb720516f564d074d55d9e2aa90e3d4e7f2 /printing | |
| parent | 231f679965745a4d7677166e8d5f62a38ebde4e7 (diff) | |
| parent | 569ad299a8092778611fcc8ae2842151c4b276db (diff) | |
Merge PR #8115: Support for custom entries in notations (take 2, feature part)
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e38da45b95..418e13759b 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -295,7 +295,7 @@ let tag_var = tag Tag.variable | CPatOr pl -> hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator - | CPatNotation ("( _ )",([p],[]),[]) -> + | CPatNotation ((_,"( _ )"),([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom | CPatNotation (s,(l,ll),args) -> @@ -665,7 +665,7 @@ let tag_var = tag Tag.variable | CastCoerce -> str ":>"), lcast ) - | CNotation ("( _ )",([t],[],[],[])) -> + | CNotation ((_,"( _ )"),([t],[],[],[])) -> return (pr (fun()->str"(") (max_int,L) t ++ str")", latom) | CNotation (s,env) -> pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env |