From 111e5edfe388d2f41ddef11800dac55b060b280b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 28 Mar 2016 15:01:05 +0200
Subject: 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.

---
 toplevel/metasyntax.ml | 7 +------
 1 file changed, 1 insertion(+), 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
-- 
cgit v1.2.3