diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-17 12:35:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:06 +0100 |
| commit | 3a6b1d2c04ceeb568accbc9ddfc3fc0f14faf25b (patch) | |
| tree | 52d6f018753666991104a6a63558b1ecef387bb8 /interp/notation.ml | |
| parent | 149997b59c6711c551490c4e7601eaac59f5f675 (diff) | |
Respecting the ident/pattern distinction in notation modifiers.
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index e6186e08c..e2e769d2f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -622,9 +622,15 @@ let availability_of_prim_token n printer_scope local_scopes = let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 +let notation_binder_source_eq s1 s2 = match s1, s2 with + | NtnParsedAsConstr, NtnParsedAsConstr -> true + | NtnParsedAsIdent, NtnParsedAsIdent -> true + | NtnParsedAsPattern, NtnParsedAsPattern -> true + | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false + let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true -| NtnTypeBinder b1, NtnTypeBinder b2 -> b1 = (b2:bool) +| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2 | NtnTypeConstrList, NtnTypeConstrList -> true | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false |