diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-10 10:04:56 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-10 10:04:56 +0100 |
| commit | 4d5c7243b4aea5b28358757e2d86c11334da6699 (patch) | |
| tree | ade1ab73a9c2066302145bb3781a39b5d46b4513 /plugins/ltac/pptactic.ml | |
| parent | 93a1c4786c9b17efdda025f754ad97376d61a9ba (diff) | |
| parent | b1d749e59444f86e40f897c41739168bb1b1b9b3 (diff) | |
Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index a42994652..5d262ffcb 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -181,9 +181,9 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_and_short_name pr (c,_) = pr c - let pr_or_by_notation f = function + let pr_or_by_notation f = CAst.with_val (function | AN v -> f v - | ByNotation {CAst.v=(s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) let pr_located pr (loc,x) = pr x |