diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/13844-gares-command-loc.sh | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
2 files changed, 3 insertions, 2 deletions
diff --git a/dev/ci/user-overlays/13844-gares-command-loc.sh b/dev/ci/user-overlays/13844-gares-command-loc.sh new file mode 100644 index 0000000000..d9a1736532 --- /dev/null +++ b/dev/ci/user-overlays/13844-gares-command-loc.sh @@ -0,0 +1 @@ +overlay elpi https://github.com/LPCIC/coq-elpi command-loc 13844 diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f3d6239c6f..f8fd8b3d5b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -576,7 +576,7 @@ let _ = let open Vernacextend in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in - let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) in + let cmd_fn c ?loc:_ ~atts = VtDefault (fun () -> in_current_context econstr_display c) in let cmd_class _ = VtQuery in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in vernac_extend ~command:"PrintConstr" [cmd] @@ -585,7 +585,7 @@ let _ = let open Vernacextend in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in - let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in + let cmd_fn c ?loc:_ ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in let cmd_class _ = VtQuery in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in vernac_extend ~command:"PrintPureConstr" [cmd] |