diff options
Diffstat (limited to 'parsing/ppextend.ml')
| -rw-r--r-- | parsing/ppextend.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index 92f44faec8..0277e79adb 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -59,7 +59,8 @@ let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ | UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false -(* Concrete syntax for symbolic-extension table *) +(* Register generic and specific printing rules *) + let generic_notation_printing_rules = Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t) |