From d44846131cf2fab2d3c45d435b84d802b1af8d43 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 15 Dec 1999 15:24:13 +0000
Subject: Nouveaux types 'constructor' et 'inductive' dans Term; les fonctions
 sur les inductifs prennent maintenant des 'inductive' en paramètres; elle
 n'ont plus besoin de faire des appels dangereux aux find_m*type qui
 centralisent la levée de raise Induc.

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

(limited to 'dev')

diff --git a/dev/changements.txt b/dev/changements.txt
index da1b10255b..d13fb1e837 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -67,7 +67,7 @@ Changements dans les fonctions :
 	  mis_lc	 ->  instantiate_lc	
 
 	Ex-Environ	 
-	  mind_path      -> Global.lookup_mind
+	  mind_of_path      -> Global.lookup_mind
 
 	Printer
 	  gentermpr	->   gen_pr_term
@@ -76,6 +76,12 @@ Changements dans les fonctions :
 	  type_of_type     ->  judge_of_type
 	  fcn_proposition  ->  judge_of_prop_contents
 
+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.
 
 Changements dans les grammaires
 -------------------------------
-- 
cgit v1.2.3