diff options
| author | Pierre-Marie Pédrot | 2016-01-11 22:20:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-14 18:23:32 +0100 |
| commit | 448866f0ec5291d58677d8fccbefde493ade0ee2 (patch) | |
| tree | 2824618cc31f7422be33f537c4ae8a8719180c53 /printing/pptactic.ml | |
| parent | 67b9b34d409c793dc449104525684852353ee064 (diff) | |
Removing constr generic argument.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index df5f57dac1..a8fa8313f2 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -267,7 +267,6 @@ module Make let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = match Genarg.genarg_tag x with - | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in @@ -295,7 +294,6 @@ module Make let rec pr_glb_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in @@ -322,7 +320,6 @@ module Make let rec pr_top_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | ConstrArgType -> prc (out_gen (topwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in @@ -1427,6 +1424,12 @@ let () = Genprint.register_print0 Constrarg.wit_sort pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 + Constrarg.wit_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; + Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr (fun (c,_) -> Printer.pr_glob_constr c) |