aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptactic.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 22:13:02 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 22:13:02 +0200
commit4b9cf206fec3ef9be52fdef67d564e3edc21eb5a (patch)
treec74f29db0ee113a17e505a734a8e04646ecc9e10 /printing/pptactic.ml
parent1093c5e758f796b9dce3d870cb05f2c8a89bef43 (diff)
Revert "Taking into account the original grammar rule to print generic"
Diffstat (limited to 'printing/pptactic.ml')
-rw-r--r--printing/pptactic.ml12
1 files changed, 1 insertions, 11 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c3c4009ca..f58452176 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -70,17 +70,6 @@ let declare_extra_genarg_pprule wit f g h =
let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in
genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule
-let find_extra_genarg_pprule wit =
- let s = match wit with
- | ExtraArg s -> ArgT.repr s
- | _ -> error
- "Can declare a pretty-printing rule only for extra argument types."
- in
- let (f,g,h) = String.Map.find s !genarg_pprule in
- (fun prc prlc prtac x -> f prc prlc prtac (in_gen (rawwit wit) x)),
- (fun prc prlc prtac x -> g prc prlc prtac (in_gen (glbwit wit) x)),
- (fun prc prlc prtac x -> h prc prlc prtac (in_gen (topwit wit) x))
-
module Make
(Ppconstr : Ppconstrsig.Pp)
(Taggers : sig
@@ -309,6 +298,7 @@ module Make
try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x)
with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x)
+
let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) =
match wit with
| ListArg wit ->