diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 16:15:32 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 16:15:32 +0100 |
commit | af291869bb7d1184d8e655906572d75937ca829b (patch) | |
tree | 62a5ccf9ee7b115b7d1118cbc3db92c553261713 /interp/notation.ml | |
parent | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (diff) | |
parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) |
Merge branch 'trunk' into pr379
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 29e5a3bfd..90ac7f729 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -927,19 +927,19 @@ let locate_notation prglob ntn scope = match ntns with | [] -> str "Unknown notation" | _ -> - t (str "Notation " ++ - tab () ++ str "Scope " ++ tab () ++ fnl () ++ + str "Notation" ++ fnl () ++ prlist (fun (ntn,l) -> let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> hov 0 ( - pr_notation_info prglob df r ++ tbrk (1,2) ++ - (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++ - tbrk (1,2) ++ - (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ()) + pr_notation_info prglob df r ++ + (if String.equal sc default_scope then mt () + else (spc () ++ str ": " ++ str sc)) ++ + (if Option.equal String.equal (Some sc) scope + then spc () ++ str "(default interpretation)" else mt ()) ++ fnl ())) - l) ntns) + l) ntns let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); |