From 2a38552ad35cdcd827da014106aa5b4af88dfb9e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 31 Oct 2018 00:12:13 +0100
Subject: Notations: fixing a bug with abbreviations in custom entries.

Coercions were missing.
---
 test-suite/output/Notations4.out | 2 ++
 test-suite/output/Notations4.v   | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index cef7d1a702..46784d1897 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -1,5 +1,7 @@
 [< 0 > + < 1 > * < 2 >]
      : nat
+[< b > + < b > * < 2 >]
+     : nat
 [<< # 0 >>]
      : option nat
 [1 {f 1}]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 9738ce5a5e..6bdbf1bed5 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -10,6 +10,10 @@ Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
 Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
 Check [ < 0 > + < 1 > * < 2 >].
 
+Axiom a : nat.
+Notation b := a.
+Check [ < b > + < a > * < 2 >].
+
 Declare Custom Entry anotherconstr.
 
 Notation "[ x ]" := x (x custom myconstr at level 6).
-- 
cgit v1.2.3