From b82cb93d2020783f72a8f99142799b51ca7991a9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 3 Oct 2010 13:12:03 +0000
Subject: Added multiple implicit arguments rules per name. Example: "Implicit
 Arguments eq_refl [[A] [x]] [[A]]".

This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/PrintInfos.out | 9 +++++++++
 test-suite/output/PrintInfos.v   | 3 +++
 test-suite/success/implicit.v    | 6 ++++++
 3 files changed, 18 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 2c20350047..19d7e7c684 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -78,3 +78,12 @@ Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
 Notation existS2 := existT2
 Expands to: Notation Coq.Init.Specif.existS2
+Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+
+For eq: Argument A is implicit and maximally inserted
+For eq_refl, when applied to no arguments:
+  Arguments A, x are implicit and maximally inserted
+For eq_refl, when applied to 1 argument:
+  Argument A is implicit and maximally inserted
+For eq: Argument scopes are [type_scope _ _]
+For eq_refl: Argument scopes are [type_scope _]
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 972caf8aa7..dd9f3c07ac 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -26,3 +26,6 @@ Print bar.
 
 About Peano. (* Module *)
 About existS2. (* Notation *)
+
+Implicit Arguments eq_refl [[A] [x]] [[A]].
+Print eq_refl.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 59e1a9352f..0aa0ae02b0 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -86,3 +86,9 @@ Fixpoint plus n m {struct n} :=
   | 0 => m
   | S p => S (plus p m)
   end.
+
+(* Check multiple implicit arguments signatures *)
+
+Implicit Arguments eq_refl [[A] [x]] [[A]].
+
+Check eq_refl : 0 = 0.
-- 
cgit v1.2.3