diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-24 12:46:57 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-24 12:46:57 +0100 |
| commit | 31794a1828a15acb95c235fd3166c511635add41 (patch) | |
| tree | fb09a6b201001ababc3030dc80fa9d729526c0a7 /dev/top_printers.ml | |
| parent | 92c15a9b660b874ce3fa125b1f9bdf2e85c40f47 (diff) | |
| parent | 57f62f06419972ba799e451d2f56552dc1b2fb63 (diff) | |
Merge PR #6197: [plugin] Remove LocalityFixme über hack.
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index df5f05469..4e7b94e41 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -509,7 +509,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ st -> in_current_context constr_display c; st) + (fun ~atts ~st -> in_current_context constr_display c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) @@ -525,7 +525,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ st -> in_current_context print_pure_constr c; st) + (fun ~atts ~st -> in_current_context print_pure_constr c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) |