From 2d871f4615e17bcb9db4edf378e725dee09331cf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 1 Sep 2006 12:17:05 +0000
Subject: Extension et réorganisation de l'interprétation des (co-)points fixes
 - Relâchement de l'exigence que les types des paramètres et le type   des
 (co-)points fixes soient donnés. Ils peuvent maintenant être   inférés à
 partir des autres informations de types. - Plus de déclaration séparée de
 celles des fonctions d'un bloc de   points fixes qui n'interviennent pas dans
 la définition des autres   (collect_non_rec): remplacement par un simple
 warning en cas de non   dépendance mutuelle de toutes les fonctions du bloc
 (de toutes   façons les fonctions qui intervenaient dans les autres sans en  
 dépendre - càd les fonctions définissables avant la partie point   fixe -
 n'étaient pas détectées) - Ajout du test de dépendance mutuel au cas des
 co-points fixes

Extension et réorganisation de l'interprétation des blocs de
définitions (co-)inductives: relâchement de l'exigence que les types
des paramètres soient donnés. Ils peuvent maintenant être inférés à
partir des autres informations des blocs d'inductifs.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9108 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/implicit.v | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 1786424e5c..47c58f0450 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -29,6 +29,10 @@ Check (fun x => fst (f x)).
 Check (fun x => fst (f x)).
 Notation rhs := snd.
 Check (fun x => snd (f x)).
-(* V8 seulement 
-Check (fun x => @ rhs ? ? (f x)).
-*)
+Check (fun x => @ rhs _ _ (f x)).
+
+(* Implicit arguments in fixpoints and inductive declarations *)
+
+Fixpoint g n := match n with O => true | S n => g n end.
+
+Inductive P n : nat -> Prop := c : P n n.
-- 
cgit v1.2.3