diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 8aad36675447f3c95dc2f10e26c4cce48595497b (patch) | |
| tree | deb34d0aebc627d31317ff8ac418f6a07f506632 | |
| parent | 172708b434ead6c3f824cf51e60c3141597e1e2b (diff) | |
Revert "Fixing printing of pat%constr."
This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c.
| -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 7b2c5695fd..5e86c6bd76 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 "<-" |