diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-09 15:03:50 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-09 15:14:23 +0200 |
| commit | 0d3c319336efaee78fb799c44806d3b9b8b28a50 (patch) | |
| tree | d6112ac2347c0b717c68141761c4e9b6be71887d | |
| parent | 3456726bd4a8ee04393bd0f89794c9fadb9649e9 (diff) | |
Fix bug #4940: Tactic notation printing could be more informative.
| -rw-r--r-- | printing/pptactic.ml | 25 |
1 files changed, 15 insertions, 10 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 917a277c9..e2c78a507 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -373,20 +373,25 @@ module Make in str "<" ++ name ++ str ">" ++ args + let rec pr_user_symbol = function + | Extend.Ulist1 tkn -> "ne_" ^ pr_user_symbol tkn ^ "_list" + | Extend.Ulist1sep (tkn, _) -> "ne_" ^ pr_user_symbol tkn ^ "_list" + | Extend.Ulist0 tkn -> pr_user_symbol tkn ^ "_list" + | Extend.Ulist0sep (tkn, _) -> pr_user_symbol tkn ^ "_list" + | Extend.Uopt tkn -> pr_user_symbol tkn ^ "_opt" + | Extend.Uentry tag -> + let ArgT.Any tag = tag in + ArgT.repr tag + | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl + let pr_alias_key key = try let prods = (KNmap.find key !prnotation_tab).pptac_prods in - (* First printing strategy: only the head symbol *) - match prods with - | TacTerm s :: prods -> str s - | _ -> - (* Second printing strategy; if ever Tactic Notation is eventually *) - (* accepting notations not starting with an identifier *) let rec pr = function - | [] -> [] - | TacTerm s :: prods -> s :: pr prods - | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in - str (String.concat " " (pr prods)) + | TacTerm s -> primitive s + | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb)) + in + pr_sequence pr prods with Not_found -> KerName.print key |