aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/syntax_def.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/syntax_def.ml')
-rw-r--r--interp/syntax_def.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 334135eaf..7790e56d5 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -74,8 +74,8 @@ type syndef_interpretation = (identifier * subscopes) list * aconstr
(* Coercions to the general format of notation that also supports
variables bound to list of expressions *)
-let in_pat (ids,ac) = ((ids,[]),ac)
-let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac)
+let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,(sc,NtnTypeConstr))) ids,ac)
+let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac)
let declare_syntactic_definition local id onlyparse pat =
let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()