diff options
| author | herbelin | 2000-03-28 16:30:04 +0000 |
|---|---|---|
| committer | herbelin | 2000-03-28 16:30:04 +0000 |
| commit | ed11f59ab67b0b6eb103d07386bf45ab2a8bede6 (patch) | |
| tree | 78d2631a84485271c91909915dfa8f96f67d5ca0 /dev | |
| parent | bc8d450ec17b6e9f40aae2ad040f296ed2f3419f (diff) | |
Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf_,}interp_constr*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@357 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/changements.txt | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/changements.txt b/dev/changements.txt index f247062e37..6293de2960 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -80,6 +80,18 @@ Changements dans les fonctions : whd_betadeltat -> whd_betaevar whd_betadeltatiota -> whd_betaiotaevar + Astterm + constr_of_com_casted -> interp_casted_constr + constr_of_com_sort -> interp_type + constr_of_com -> interp_constr + rawconstr_of_com -> interp_rawconstr + type_of_com -> typed_type_of_com + + Tacmach + pf_constr_of_com_sort -> pf_interp_type + pf_constr_of_com -> pf_interp_constr + + Changements dans les inductifs ------------------------------ Nouveaux types "constructor" et "inductive" dans Term |