diff options
| author | Gaëtan Gilbert | 2019-10-28 17:55:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-31 14:42:54 +0100 |
| commit | 82bdd64c97f45510044a9ccd9b5b87effcd034d1 (patch) | |
| tree | 9c95727492317912b89966d93ef1aaca45cf7e5e /vernac/ppvernac.ml | |
| parent | 215b7e43cba768bfc82914718b159a22797f9d2b (diff) | |
Print argument info as an Arguments command in About
Close #10961
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f91983d31c..5cffc39839 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1083,7 +1083,12 @@ let string_of_definition_object_kind = let open Decls in function match n, nbidi, l with | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l | _, Some 0, l -> spc () ++ str"|" ++ print_arguments n None l - | _, _, [] -> mt() + | None, None, [] -> mt() + | _, _, [] -> + let dummy = {name=Anonymous; recarg_like=false; + notation_scope=None; implicit_status=Impargs.NotImplicit} + in + print_arguments n nbidi [dummy] | n, nbidi, { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> |