diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
| commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
| tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /interp/syntax_def.ml | |
| parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) | |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 884dea48..fe998cba 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: syntax_def.ml 10730 2008-03-30 21:42:58Z herbelin $ *) +(* $Id: syntax_def.ml 11512 2008-10-27 12:28:36Z herbelin $ *) open Util open Pp @@ -70,11 +70,18 @@ let (in_syntax_constant, out_syntax_constant) = classify_function = classify_syntax_constant; export_function = export_syntax_constant } +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 declare_syntactic_definition local id onlyparse pat = - let _ = add_leaf id (in_syntax_constant (local,pat,onlyparse)) in () + let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () let search_syntactic_definition loc kn = - KNmap.find kn !syntax_table + out_pat (KNmap.find kn !syntax_table) let locate_global_with_alias (loc,qid) = match Nametab.extended_locate qid with |