aboutsummaryrefslogtreecommitdiffhomepage
path: root/translate/ppconstrnew.ml
diff options
context:
space:
mode:
Diffstat (limited to 'translate/ppconstrnew.ml')
-rw-r--r--translate/ppconstrnew.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index af8fb845d..8104399c0 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -351,12 +351,17 @@ let tm_clash = function
let pr_case_item pr (tm,(na,indnalopt)) =
hov 0 (pr (lcast,E) tm ++
+(*
(match na with
| Name id when not (is_var id tm) -> spc () ++ str "as " ++ pr_id id
| Anonymous when tm_clash (tm,indnalopt) <> None ->
(* hide [tm] name to avoid conflicts *)
spc () ++ str "as _" (* ++ pr_id (out_some (tm_clash (tm,indnalopt)))*)
| _ -> mt ()) ++
+*)
+ (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
+ | Some na -> spc () ++ str "as " ++ pr_name na
+ | None -> mt ()) ++
(match indnalopt with
| None -> mt ()
(*