Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :

- si on met Rle_ge et Rge_le tous les deux en Resolve (et de même
  pour Rlt_gt et Rgt_lt) alors on introduit un cycle,
- si on en met un des deux en Immediate, alors on perd la symétrie car si
  un développement n'a un lemme en hints que pour Rge (resp Rle),
  alors il ne sera pas utilisable si on met Rge_le (resp Rle_ge) en Immediate
  (et c'est ce qui arrive notamment dans HighSchoolGeometry).
L'idéal serait d'introduire une notion de raisonnement modulo équivalence 
dans auto afin que chaque lemme sur Rle (resp Rge) soit systématiquement 
applicable aussi face à Rge (resp Rle) sans redondances et sans
cycle. Ainsi Rle_ge and co n'auraient pas un statut de hints mais plutôt un
statut de conversions implicites entre notions synonymes.


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

0 files changed, 0 insertions, 0 deletions