diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 190181c23..1d03716d0 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -17,7 +17,6 @@ open Ppextend open Constrexpr open Constrexpr_ops open Topconstr -open Term open Decl_kinds open Misctypes open Locus @@ -34,7 +33,6 @@ let lif = 200 let lletin = 200 let lletpattern = 200 let lfix = 200 -let larrow = 90 let lcast = 100 let larg = 9 let lapp = 10 @@ -612,7 +610,6 @@ let pr_red_flag pr r = pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) - let pr_metaid id = str"?" ++ pr_id id let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function |