Retour en arrière pour raison de compatibilité sur la suppression du nf_evar

dans clos_norm_flags (cf échec dans CoRN.Transc.InvTrigonom.Tan_ilim). Ceci 
dit :
- cela ne me parait pas moral que clos_norm_flags s'occupe de
  normaliser les evars,
- mais comme "evar" n'est pas un flag supporté par closure.ml, on ne 
  peut pas le donner à la demande comme argument de clos_norm_flags
  (question: pourrait-on faire supporter la réduction Evar par closure.ml ??).

Plus généralement, il y a un problème avec la propagation des
instantiations des evars à travers les buts (cf lemme eapply_evar dans
test-suite/success/apply.v).



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

0 files changed, 0 insertions, 0 deletions