From 3df82e1adcfb96320b3fbbb622d9e54cb0a176e1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Aug 2020 12:25:36 +0200
Subject: In "About", print all arguments, even if it is trailing list of _.

---
 vernac/prettyp.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3