diff options
| author | herbelin | 2000-10-11 20:11:38 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-11 20:11:38 +0000 |
| commit | 23b561d63073f0193caa63c953ca3176a1a4fb47 (patch) | |
| tree | 4365db198a3df7d676a27a67142b82bd3383a13b /dev | |
| parent | 2d9aa9c7f84c3a48c870c354cb1a794e7423db50 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@700 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/changements.txt | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/dev/changements.txt b/dev/changements.txt index c2b12d2175..f94e534560 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -93,6 +93,9 @@ Changements dans les fonctions : Reduction, Clenv whd_betadeltat -> whd_betaevar whd_betadeltatiota -> whd_betaiotaevar + find_mrectype -> Inductive.find_mrectype + find_minductype -> Inductive.find_inductive + find_mcoinductype -> Inductive.find_coinductive Astterm constr_of_com_casted -> interp_casted_constr @@ -155,7 +158,7 @@ Changements dans les inductifs Nouveaux types "constructor" et "inductive" dans Term La plupart des fonctions de typage des inductives prennent maintenant un inductive au lieu d'un oonstr comme argument. Les seules fonctions -à traduite un constr en inductive sont les find_mrectype and co. +à traduire un constr en inductive sont les find_rectype and co. Changements dans les grammaires ------------------------------- |