diff options
| author | Hugo Herbelin | 2016-04-13 15:16:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:46 +0200 |
| commit | 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c (patch) | |
| tree | faf3943ea63e9955f165cc5d5c85079cd0da3b88 | |
| parent | 23ebfc41fba48ccce9bc878de258d1b0901f7dda (diff) | |
Fixing printing of pat%constr.
| -rw-r--r-- | printing/miscprint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/miscprint.ml b/printing/miscprint.ml index 5e86c6bd76..7b2c5695fd 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -28,7 +28,7 @@ and pr_intro_pattern_action prc = function | IntroInjection pl -> str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ str "]" - | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "/" ++ prc c + | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c | IntroRewrite true -> str "->" | IntroRewrite false -> str "<-" |