From fc06cb87286e2b114c7f92500511d5914b8f7f48 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 22 Jul 2010 21:06:18 +0000 Subject: Extension of the recursive notations mechanism - Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/syntax_def.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp/syntax_def.ml') 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 () -- cgit v1.2.3