diff options
| author | Hugo Herbelin | 2020-07-27 22:15:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-09 02:48:26 +0200 |
| commit | 80a95afb14fce55781bf7ded5a65233a3f3192b0 (patch) | |
| tree | b86f1ac2d9aa25913fd0093af0d57fdac684463e | |
| parent | 9d8efb01fde0f9e24157872213c0595cc72efc0c (diff) | |
Fixing a coercion entry transitivity bug.
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 15 |
3 files changed, 18 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index c4e9496b95..0bd5da5729 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1429,7 +1429,7 @@ let declare_entry_coercion (scope,(entry,key)) lev entry' = let toaddright = EntryCoercionMap.fold (fun (entry'',entry''') paths l -> List.fold_right (fun ((lev'',lev'''),path) l -> - if entry' = entry'' && level_ord lev' lev'' && entry <> entry''' + if entry' = entry'' && level_ord lev'' lev' && entry <> entry''' then ((entry,entry'''),((lev,lev'''),path@[(scope,(entry,key))]))::l else l) paths l) !entry_coercion_map [] in entry_coercion_map := diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index fa03ec8193..ce51acac95 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -123,3 +123,5 @@ File "stdin", line 297, characters 0-30: Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] 0 :=: 0 : Prop +fun x : nat => <{ x; (S x) }> + : nat -> nat diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 90d8da2bec..73445bad12 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -298,3 +298,18 @@ Notation "x :=: y" := (x = y). Check (0 :=: 0). End Bug12691. + +Module CoercionEntryTransitivity. + +Declare Custom Entry com. +Declare Custom Entry com_top. +Notation "<{ e }>" := e (at level 0, e custom com_top at level 99). +Notation "x ; y" := + (x + y) + (in custom com_top at level 90, x custom com at level 90, right associativity). +Notation "x" := x (in custom com at level 0, x constr at level 0). +Notation "x" := x (in custom com_top at level 90, x custom com at level 90). + +Check fun x => <{ x ; (S x) }>. + +End CoercionEntryTransitivity. |