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

0 files changed, 0 insertions, 0 deletions