diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2entries.ml | 1 |
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; |