2 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 38c5b827fd..7949ef7b2c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -8,3 +8,7 @@ d2 = fun x : nat => d1 (y:=x)
 
 Arguments x, x0 are implicit
 Argument scopes are [nat_scope nat_scope _]
+map id (1 :: nil)
+     : list nat
+map id' (1 :: nil)
+     : list nat
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 0ff7e87f37..4c6f2b5dd9 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -17,3 +17,22 @@ Definition d1 y x (h : x = y :>nat) := h.
 Definition d2 x := d1 (y:=x).
 
 Print d2.
+
+(* Check maximal insertion of implicit *)
+
+Require Import List.
+
+Open Scope list_scope.
+
+Set Implicit Arguments.
+Set Maximal Implicit Insertion.
+
+Definition id (A:Type) (x:A) := x.
+
+Check map id (1::nil).
+
+Definition id' (A:Type) (x:A) := x.
+
+Implicit Arguments id' [[A]].
+
+Check map id' (1::nil).