diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 8bdea1356..d16035fba 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -220,7 +220,6 @@ let rec pr_glob_generic prc prlc prtac prpat x = try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x with Not_found -> str "[no printer for " ++ str s ++ str "]" - let rec pr_generic prc prlc prtac prpat x = match Genarg.genarg_tag x with | BoolArgType -> str (if out_gen wit_bool x then "true" else "false") @@ -549,7 +548,6 @@ let linfo = 5 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq - (** A printer for tactics that polymorphically works on the three "raw", "glob" and "typed" levels; in practice, the environment is used only at the glob and typed level: it is used to feed the |