diff options
| author | herbelin | 2000-09-06 17:10:38 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-06 17:10:38 +0000 |
| commit | 48e922f2af1927b84801ea3781ba0acb30c0dd7f (patch) | |
| tree | 45dc2c10c7c5beed25dc4f7296534c342f95d05c /dev | |
| parent | 48af8fc25bdad1b8c2f475db67ff574e2311d641 (diff) | |
Canonisation de certains noms dans Pretyping, Asterm et Safe_typing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/changements.txt | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/dev/changements.txt b/dev/changements.txt index e54858016c..dc9b01b17b 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -83,6 +83,7 @@ Changements dans les fonctions : Typing, Machops type_of_type -> judge_of_type fcn_proposition -> judge_of_prop_contents + safe_fmachine -> safe_infer Reduction, Clenv whd_betadeltat -> whd_betaevar @@ -93,7 +94,8 @@ Changements dans les fonctions : constr_of_com_sort -> interp_type constr_of_com -> interp_constr rawconstr_of_com -> interp_rawconstr - type_of_com -> typed_type_of_com + type_of_com -> type_judgement_of_rawconstr + judgement_of_com -> judgement_of_rawconstr Termast bdize -> ast_of_constr @@ -134,9 +136,11 @@ Changements dans les fonctions : Declare machine_constant -> declare_constant (+ modifs) - ex-Trad + ex-Trad, maintenant Pretyping inh_cast_rel -> Coercion.inh_conv_coerce_to inh_conv_coerce_to -> Coercion.inh_conv_coerce_to_fail + ise_resolve1 -> ise_resolve, ise_resolve_type + ise_resolve -> ise_infer, ise_infer_type Changements dans les inductifs ------------------------------ |