Améliorations de l'affichage des coercions suggérées par Georges :

- Suppression d'un hack bancal qui permettait d'afficher des notations
  dont les arguments du premier niveau applicatif n'étaient pas
  syntaxiquement entourés de coercions dans la définition de la
  notation alors qu'ils ne pouvaient que l'être dans les termes
  effectifs (ex: 'Notation ... := (true /\ True)' pouvait être reconnu
  malgré l'absence de la coercion de bool vers Prop).

- Propagation de l'information "in context" aux branches des
  if/let/match par symmétrie avec l'inférence de type qui propage
  l'information EXTERNE de type vers les branches (stratégie moins
  "défensive" pour la suppression des coercions).



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

0 files changed, 0 insertions, 0 deletions