From 23b561d63073f0193caa63c953ca3176a1a4fb47 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Oct 2000 20:11:38 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@700 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/changements.txt | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'dev')

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
 -------------------------------
-- 
cgit v1.2.3