- New cleaning phase for the entry points of pretyping.ml

- Uniformisation of ML names between pretyping.ml and subtac_pretyping_F.ml 
  so as to ease the comparison between these files. Application of a
  change that cannot do harm: j_nf_evar now called after getting evd
  from consider_remaining_unif_problems in
  Subtac_pretyping_F.understand_judgment. Four differences remain
  (is it the sign of a problem?):
  1) understand_type fails in Pretyping if evars remain but does not fail in
     Subtac_pretyping_F
  2) resolve_typeclasses (when called) is called with ~onlyargs:false and 
     ~fail:true in Pretyping.understand, Pretyping.understand_gen and
     Pretyping.understand_type but with true and false in these same
     functions in Subtac_pretyping_F
  3) understand_ltac does not call typeclasses in Pretyping but it
     does call it in Subtac_pretyping_F
  4) understand_judgment does call typeclasses in Pretyping but not in
     Subtac_pretyping_F



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

0 files changed, 0 insertions, 0 deletions