1 files changed, 8 insertions, 11 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ce8798c713..42f65dfb52 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -890,12 +890,12 @@ let warn_non_reversible_notation =
          (fun () ->
           strbrk "This notation will not be used for printing as it is not reversible.")
 
-let is_not_printable onlyparse noninjective = function
+let is_not_printable onlyparse nonreversible = function
 | NVar _ ->
   if not onlyparse then warn_notation_bound_to_variable ();
   true
 | _ ->
-   if not onlyparse && noninjective then
+   if not onlyparse && nonreversible then
      (warn_non_reversible_notation (); true)
   else onlyparse
 
@@ -1182,12 +1182,11 @@ let add_notation_in_scope local df c mods scope =
   let nenv = {
     ninterp_var_type = to_map i_vars;
     ninterp_rec_vars = to_map recvars;
-    ninterp_only_parse = false;
   } in
-  let (acvars, ac) = interp_notation_constr nenv c in
+  let (acvars, ac, reversible) = interp_notation_constr nenv c in
   let interp = make_interpretation_vars recvars acvars in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
-  let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in
+  let onlyparse = is_not_printable onlyparse (not reversible) ac in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
@@ -1222,12 +1221,11 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
   let nenv = {
     ninterp_var_type = to_map i_vars;
     ninterp_rec_vars = to_map recvars;
-    ninterp_only_parse = false;
   } in
-  let (acvars, ac) = interp_notation_constr ~impls nenv c in
+  let (acvars, ac, reversible) = interp_notation_constr ~impls nenv c in
   let interp = make_interpretation_vars recvars acvars in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
-  let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in
+  let onlyparse = is_not_printable onlyparse (not reversible) ac in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
@@ -1364,10 +1362,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
       let nenv = {
         ninterp_var_type = i_vars;
         ninterp_rec_vars = Id.Map.empty;
-        ninterp_only_parse = false;
       } in
-      let nvars, pat = interp_notation_constr nenv c in
-      let () = nonprintable := nenv.ninterp_only_parse in
+      let nvars, pat, reversible = interp_notation_constr nenv c in
+      let () = nonprintable := not reversible in
       let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in
       List.map map vars, pat
   in