From 2f95db622428cf58968e8d13f2230fe51c31e97f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 30 Oct 2017 18:11:26 +0100
Subject: Put notations in level 5 by default.

---
 src/tac2entries.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src')

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;
-- 
cgit v1.2.3