diff options
| author | Hugo Herbelin | 2018-10-23 16:33:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-13 22:37:01 +0200 |
| commit | 466e6737de8772f46f08ea8e38fda196993597c0 (patch) | |
| tree | 93b5bf81ba3be2f0094a67546366b9ddd98c333f /interp/syntax_def.ml | |
| parent | 91b5990e724acc863a5dba66acc33fd698ac26f0 (diff) | |
Extending support for mixing binders and terms in abbreviations.
Diffstat (limited to 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 16 |
1 files changed, 3 insertions, 13 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 7184f5ea29..bd3e234a91 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Pp open CErrors open Names @@ -82,16 +81,9 @@ let in_syntax_constant : (bool * syndef) -> obj = subst_function = subst_syntax_constant; classify_function = classify_syntax_constant } -type syndef_interpretation = (Id.t * subscopes) list * notation_constr - -(* Coercions to the general format of notation that also supports - variables bound to list of expressions *) -let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac) -let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) - let declare_syntactic_definition ~local deprecation id ~onlyparsing pat = let syndef = - { syndef_pattern = in_pat pat; + { syndef_pattern = pat; syndef_onlyparsing = onlyparsing; syndef_deprecation = deprecation; } @@ -106,14 +98,12 @@ let warn_deprecated_syntactic_definition = let search_syntactic_definition ?loc kn = let syndef = KNmap.find kn !syntax_table in - let def = out_pat syndef.syndef_pattern in Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; - def + syndef.syndef_pattern let search_filtered_syntactic_definition ?loc filter kn = let syndef = KNmap.find kn !syntax_table in - let def = out_pat syndef.syndef_pattern in - let res = filter def in + let res = filter syndef.syndef_pattern in if Option.has_some res then Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation; res |