diff options
author | 2009-04-24 09:29:08 +0000 | |
---|---|---|
committer | 2009-04-24 09:29:08 +0000 | |
commit | 8bc5a17d7beb67a68befe2fcd73932d477d1925f (patch) | |
tree | 71f450688ec9239b8ce016d932b1b3f9a0641c5a /tools/coqdoc/output.ml | |
parent | 339fad94cbb51911698142e3e879c53fa6a0e012 (diff) |
- 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
Diffstat (limited to 'tools/coqdoc/output.ml')
0 files changed, 0 insertions, 0 deletions