diff options
| author | Hugo Herbelin | 2020-08-22 12:25:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 3df82e1adcfb96320b3fbbb622d9e54cb0a176e1 (patch) | |
| tree | 849dfdb0de3fba55f483a6f07a70fa54555c0d05 /vernac | |
| parent | 911f33f0a0ff648082d329841388f59e8cecf231 (diff) | |
In "About", print all arguments, even if it is trailing list of _.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/prettyp.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 2b46542287..d84165d032 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -268,8 +268,10 @@ let dummy = { notation_scope = None; } -let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = - name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit +let is_dummy = function + | Vernacexpr.(RealArg {implicit_status; name; recarg_like; notation_scope}) -> + name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit + | _ -> false let rec main_implicits i renames recargs scopes impls = if renames = [] && recargs = [] && scopes = [] && impls = [] then [] @@ -292,9 +294,7 @@ let rec main_implicits i renames recargs scopes impls = let tl = function [] -> [] | _::tl -> tl in (* recargs is special -> tl handled above *) let rest = main_implicits (i+1) (tl renames) recargs (tl scopes) (tl impls) in - if is_dummy status && rest = [] - then [] (* we may have a trail of dummies due to eg "clear scopes" *) - else status :: rest + status :: rest let rec insert_fake_args volatile bidi impls = let open Vernacexpr in @@ -336,7 +336,7 @@ let print_arguments ref = let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in let bidi = Pretyping.get_bidirectionality_hint ref in let impls = insert_fake_args nargs_for_red bidi impls in - if impls = [] && moreimpls = [] && flags = [] then [] + if List.for_all is_dummy impls && moreimpls = [] && flags = [] then [] else let open Constrexpr in let open Vernacexpr in |