Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).

Was broken since 8.6.

3 files changed, 41 insertions, 6 deletions

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index bc0de0acd..3f885f8ba 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
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 35c3057d8..c5d58ec1e 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -31,3 +31,10 @@ nat
 nat
 0
 0
+Ltac foo :=
+  let x := intros ** in
+  let y := intros -> in
+  let v := constr:(nil) in
+  let w := () in
+  let z := 1 in
+  pose v
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 76c37625a..6adbe95dd 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -57,3 +57,14 @@ match goal with |- ?x*?y => idtac x end.
 match goal with H: context [?x*?y] |- _ => idtac x end.
 match goal with |- context [?x*?y] => idtac x end.
 Abort.
+
+(* Check printing of let in Ltac and Tactic Notation *)
+
+Ltac foo :=
+  let x := intros in
+  let y := intros -> in
+  let v := constr:(@ nil True) in
+  let w := () in
+  let z := 1 in
+  pose v.
+Print Ltac foo.