diff options
Diffstat (limited to 'contrib/field/field.ml4')
| -rw-r--r-- | contrib/field/field.ml4 | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 49a187caa..c67dea9aa 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -107,6 +107,19 @@ let _ = Tacinterp.add_genarg_interp "minus_div_arg" (in_gen (wit_pair (wit_opt rawwit_constr) (wit_opt rawwit_constr)) (out_gen rawwit_minus_div_arg x)))))) +open Ppconstrnew +let pp_minus_div_arg (omin,odiv) = str "still no printer for minus_div_arg" +let pp_raw_minus_div_arg (omin,odiv) = + if omin=None && odiv=None then mt() else + spc() ++ str "with" ++ + pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++ + pr_opt (fun c -> str "div := " ++ pr_constr c) odiv + +let () = + Pptactic.declare_extra_genarg_pprule true + (rawwit_minus_div_arg,pp_raw_minus_div_arg) + (wit_minus_div_arg,pp_minus_div_arg) + open Pcoq.Constr GEXTEND Gram GLOBAL: minus_div_arg; |