Nouveaux changements autour des implicites (notamment suite à

discussion avec Georges)

- La notion d'insertion maximale n'est plus globale mais attachée à
  chaque implicite
- Correction de petits bugs dans le calcul des implicites
- Raffinement de la notion "sous contexte" pour l'affichage des coercions



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7

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).