Put notations in level 5 by default.

1 files changed, 1 insertions, 0 deletions

diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 3ac3d14ef3..cefb4b13b8 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -674,6 +674,7 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with
   let ids = List.fold_left fold Id.Set.empty entries in
   (** Globalize so that names are absolute *)
   let body = Tac2intern.globalize ids body in
+  let lev = match lev with Some _ -> lev | None -> Some 5 in
   let ext = {
     synext_tok = tkn;
     synext_exp = body;