diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-13 15:16:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:30:18 +0200 |
| commit | b2991bf6eec4ae7706f3dd33941af909f36f1773 (patch) | |
| tree | 9719b20a35bf489b09db17418a89f7ccd48e6a28 /printing | |
| parent | f5352b71c1a7d313a70c370c631c61a8fae5599b (diff) | |
Fixing printing of pat%constr.
Diffstat (limited to 'printing')
| -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 5e86c6bd7..7b2c5695f 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 "<-" |