diff options
| author | Maxime Dénès | 2017-11-06 11:20:30 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-06 11:20:30 +0100 |
| commit | c757ec96e2f281e618c297ffc6098aacf1e3f399 (patch) | |
| tree | 9de3aaa4fb91053c8e7e3ce19c0f46390036027f /dev | |
| parent | 54057085f18fbd4c1cb0f0f01c03c08a8cc541c3 (diff) | |
| parent | f874a292c94b290a31af8e0f707ffd20ab31001b (diff) | |
Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules
Diffstat (limited to 'dev')
| -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 70f7c4283f..35956477df 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -503,7 +503,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun () -> in_current_context constr_display c) + (fun _ -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) @@ -519,7 +519,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun () -> in_current_context print_pure_constr c) + (fun _ -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) |