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

1 files changed, 7 insertions, 3 deletions

diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 1786424e5..47c58f045 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.