From 90252e973f5bcafc5f3b0b18564612d7fb4503a8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 13 Apr 2016 15:01:40 +0200
Subject: Temporary hack to restore missing printing of "constr:" in right-hand
 side of Ltac's "let ... in ..." or "match ... with ... => ... end".

Example:

Ltac f x := let x := 0 in constr:(S x).
Print Ltac f.

has a missing "constr:".

Note: for generic arguments: "ltac:" is always used, even if a constr, etc.
---
 printing/pptactic.ml | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 920f1d62a..f58452176 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -949,6 +949,13 @@ module Make
 
     let make_pr_tac pr strip_prod_binders tag_atom tag =
 
+        let pr_ltac_constr pr = function
+          | TacArg (_,TacGeneric arg)
+          | TacArg (_,Tacexp (TacArg (_,TacGeneric arg))) as u
+              when argument_type_eq (genarg_tag arg) (ArgumentType wit_constr)
+                -> keyword "constr:" ++ surround (pr u)
+          | u -> pr u in
+
         let extract_binders = function
           | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
           | body -> ([],body) in
@@ -967,9 +974,10 @@ module Make
               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_ltac_constr (pr_tac ltop)) llc
                   ++ spc () ++ keyword "in"
-                 ) ++ fnl () ++ pr_tac (llet,E) u),
+                 ) ++ fnl ()
+                 ++ pr_ltac_constr (pr_tac (llet,E)) u),
               llet
             | TacMatch (lz,t,lrul) ->
               hov 0 (
@@ -977,7 +985,7 @@ module Make
                 ++ pr_tac ltop t ++ spc () ++ keyword "with"
                 ++ prlist (fun r ->
                   fnl () ++ str "| "
-                  ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r
+                  ++ pr_match_rule true (pr_ltac_constr (pr_tac ltop)) pr.pr_lpattern r
                 ) lrul
                 ++ fnl() ++ keyword "end"),
               lmatch
@@ -987,14 +995,14 @@ module Make
                 ++ keyword (if lr then "match reverse goal with" else "match goal with")
                 ++ prlist (fun r ->
                   fnl () ++ str "| "
-                  ++ pr_match_rule false (pr_tac ltop) pr.pr_lpattern r
+                  ++ pr_match_rule false (pr_ltac_constr (pr_tac ltop)) pr.pr_lpattern r
                 ) lrul ++ fnl() ++ keyword "end"),
               lmatch
             | TacFun (lvar,body) ->
               hov 2 (
                 keyword "fun"
                 ++ prlist pr_funvar lvar ++ str " =>" ++ spc ()
-                ++ pr_tac (lfun,E) body),
+                ++ pr_ltac_constr (pr_tac (lfun,E)) body),
               lfun
             | TacThens (t,tl) ->
               hov 1 (
-- 
cgit v1.2.3