A fix to #3709: ensuring extra parentheses when a tactic entry has a

subentry at a higher tactic level than the entry itself.

This is applicable to the parsing of expressions with infix or postfix
operators such as ; or ||.

Could be improved, e.g. so that no parenthesis are put when the
expression is the rightmost one, as in:

  now (tac1;tac2)

where parentheses are not needed but still printed with this patch,
while the patch adds needed parentheses in

  (now tac1);tac2

This would hardly scale to more complex grammars. E.g., if a suffix
expression can extend a leading expression as part of different
grammar entries, as in

  let x := simpl in y ...

I don't see in general how to anticipate the need for parentheses
without restarting the parser to check the reversibility of the
printing.

1 files changed, 18 insertions, 0 deletions

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index f94f84a73b..ef09ea436d 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -285,6 +285,23 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
        subst_function = subst_tactic_notation;
        classify_function = classify_tactic_notation}
 
+let rec safe_printing_level n prods =
+  match List.last prods with
+  | TacTerm _ -> n
+  | TacNonTerm (_, (nt, sep), _) ->
+     let level = match parse_user_entry nt sep with
+     | Extend.Uentryl ("tactic",n') -> Some n'
+     | Extend.Uentry ("tactic") -> Some 5
+     | Extend.Uentry ("binder_tactic") -> Some 5
+     | _ -> None in
+     match level with
+     | Some n' when n' > n ->
+         msg_warning (strbrk "Notation ends with a tactic at a level "
+           ++ strbrk "higher than the tactic itself. Using this level "
+           ++ strbrk "for ensuring correct parenthesizing when printing.");
+         n'
+     | _ -> n
+
 let cons_production_parameter = function
 | TacTerm _ -> None
 | TacNonTerm (_, _, id) -> Some id
@@ -305,6 +322,7 @@ let add_glob_tactic_notation local n prods forml ids tac =
 
 let add_tactic_notation local n prods e =
   let ids = List.map_filter cons_production_parameter prods in
+  let printing_level = safe_printing_level n prods in
   let prods = List.map (interp_prod_item n) prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
   add_glob_tactic_notation local n prods false ids tac