diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-02-28 18:28:14 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-02-28 18:55:57 +0100 |
| commit | 4d25b224b91959b85fcd68c825a307ec684f0bac (patch) | |
| tree | 0754a149655d3c1f44be314341600f6b4515d4f5 /interp/notation.ml | |
| parent | 4fcd7fd68986246adb666ed46d066fcf0355bf09 (diff) | |
Printing notations: Cleaning in anticipation of fixing #4592.
- Making a clear distinction between expressions of the notation which
are associated to binding variables only (as in `Notation "'lam' x ,
P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2
(fun x:t => p) (fun x:t => q))') and those which are associated to
at list one subterm (e.g. `Notation "x .+1" := (S x)' but also
"Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))'
as in #4592). The former have type NtnTypeOnlyBinder.
- Thus avoiding in particular encoding too early Anonymous as GHole
and "Name id" as "GVar id".
There is a non-trivial alpha-conversion work to do to get #4592
working. See comments in Notation_ops.add_env.
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 5c10e0af7..04918bf7d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -529,9 +529,10 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true +| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true | NtnTypeConstrList, NtnTypeConstrList -> true | NtnTypeBinderList, NtnTypeBinderList -> true -| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false +| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) = |