Was too restrictive in syntactic definitions, not imagining that they

could be used with arguments which are binding variables, as was done
in ssrfun.v.

1 files changed, 1 insertions, 6 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6277a8146a..7c1f05cd3e 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1299,12 +1299,7 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
       } in
       let nvars, pat = interp_notation_constr nenv c in
       let () = nonprintable := nenv.ninterp_only_parse in
-      let map id =
-        let (isonlybinding,sc, _) = Id.Map.find id nvars in
-        (* if a notation contains an ltac:, the body is not analyzed
-           and onlybinding detection fails *)
-        assert (!nonprintable || not isonlybinding);
-        (id, sc) in
+      let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in
       List.map map vars, pat
   in
   let onlyparse = match onlyparse with