From a83c37de529f12348cd9e3a66a38c58b72777478 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Nov 2017 15:24:16 +0100
Subject: Fixes #5787 (printing of "constr:" lost in the move of constr to
 Generic).

Was broken since 8.6.
---
 plugins/ltac/pptactic.ml | 29 +++++++++++++++++++++++------
 1 file changed, 23 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index bc0de0acdf..3f885f8baa 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -84,6 +84,14 @@ type 'a extra_genarg_printer =
     (tolerability -> Val.t -> Pp.t) ->
     'a -> Pp.t
 
+let string_of_genarg_arg (ArgumentType arg) =
+  let rec aux : type a b c. (a, b, c) genarg_type -> string = function
+  | ListArg t -> aux t ^ "_list"
+  | OptArg t -> aux t ^ "_opt"
+  | PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *)
+  | ExtraArg s -> ArgT.repr s in
+  aux arg
+
   let keyword x = tag_keyword (str x)
   let primitive x = tag_primitive (str x)
 
@@ -536,15 +544,24 @@ let pr_goal_selector ~toplevel s =
 
   let pr_funvar n = spc () ++ Name.print n
 
-  let pr_let_clause k pr (na,(bl,t)) =
+  let pr_let_clause k pr_gen pr_arg (na,(bl,t)) =
+    let pr = function
+      | TacGeneric arg ->
+         let name = string_of_genarg_arg (genarg_tag arg) in
+         if name = "unit" || name = "int" then
+           (* Hard-wired parsing rules *)
+           pr_gen  arg
+         else
+           str name ++ str ":" ++ surround (pr_gen arg)
+      | _ -> pr_arg (TacArg (Loc.tag t)) in
     hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++
-             str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t)))
+             str " :=" ++ brk (1,1) ++ pr t)
 
-  let pr_let_clauses recflag pr = function
+  let pr_let_clauses recflag pr_gen pr = function
     | hd::tl ->
       hv 0
-        (pr_let_clause (if recflag then "let rec" else "let") pr hd ++
-           prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl)
+        (pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++
+           prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen pr t) tl)
     | [] -> anomaly (Pp.str "LetIn must declare at least one binding.")
 
   let pr_seq_body pr tl =
@@ -858,7 +875,7 @@ let pr_goal_selector ~toplevel s =
               let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
               v 0
                 (hv 0 (
-                  pr_let_clauses recflag (pr_tac ltop) llc
+                  pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc
                   ++ spc () ++ keyword "in"
                  ) ++ fnl () ++ pr_tac (llet,E) u),
               llet
-- 
cgit v1.2.3