Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 0ff7e87f..4c6f2b5d 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).