From 8aad36675447f3c95dc2f10e26c4cce48595497b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:03 +0200
Subject: Revert "Fixing printing of pat%constr."

This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c.
---
 printing/miscprint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 "<-"
 
-- 
cgit v1.2.3