diff options
| author | Maxime Dénès | 2019-03-01 15:27:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-03-20 09:33:15 +0100 |
| commit | 27d453641446b3d35aa2211b94f949b57a88ebb2 (patch) | |
| tree | af47b4cb0e3fbb7fde26b6cab3a9b78b99699e94 /coqpp/coqpp_main.ml | |
| parent | e5a2f0452cf9523bc86e71ae6d2ac30883a28be6 (diff) | |
Stop accessing proof env via Pfedit in printers
This should make https://github.com/coq/coq/pull/9129 easier.
Diffstat (limited to 'coqpp/coqpp_main.ml')
| -rw-r--r-- | coqpp/coqpp_main.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index cc76c44651..d33eef135f 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -493,7 +493,7 @@ let print_ast fmt arg = let pr fmt () = fprintf fmt "Vernacextend.vernac_argument_extend ~name:%a @[{@\n\ Vernacextend.arg_parsing = %a;@\n\ - Vernacextend.arg_printer = %a;@\n}@]" + Vernacextend.arg_printer = fun env sigma -> %a;@\n}@]" print_string name print_rules (name, arg.vernacargext_rules) print_printer arg.vernacargext_printer in @@ -579,7 +579,7 @@ let print_ast fmt arg = Tacentries.arg_intern = @[%a@];@\n\ Tacentries.arg_subst = @[%a@];@\n\ Tacentries.arg_interp = @[%a@];@\n\ - Tacentries.arg_printer = @[((%a), (%a), (%a))@];@\n}@]" + Tacentries.arg_printer = @[((fun env sigma -> %a), (fun env sigma -> %a), (fun env sigma -> %a))@];@\n}@]" print_string name VernacArgumentExt.print_rules (name, arg.argext_rules) pr_tag arg.argext_type |