diff options
| author | herbelin | 2009-04-24 09:29:08 +0000 |
|---|---|---|
| committer | herbelin | 2009-04-24 09:29:08 +0000 |
| commit | 8bc5a17d7beb67a68befe2fcd73932d477d1925f (patch) | |
| tree | 71f450688ec9239b8ce016d932b1b3f9a0641c5a /pretyping/pretyping.mli | |
| 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 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index e7a8374b52..974cba1b4d 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -97,7 +97,7 @@ sig rawconstr -> unsafe_type_judgment val pretype_gen : - evar_defs ref -> env -> + bool -> bool -> evar_defs ref -> env -> var_map * (identifier * identifier option) list -> typing_constraint -> rawconstr -> constr |