From f99150300603ce0d87db716efc52fa88967d4460 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 1 Dec 1999 23:13:01 +0000
Subject: Intégration du Termast et du Retyping de HH, et modifications
 connexes

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

(limited to 'dev')

diff --git a/dev/changements.txt b/dev/changements.txt
index 0e0ae4f1c5..80698a0be8 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -46,7 +46,8 @@ Changements dans les fonctions :
 	  rev_append	 ->  List.rev_append
 
 	Termenv
-	  mind_specif_of_mind  ->  Global.lookup_mind_specif
+	  mind_specif_of_mind  -> Global.lookup_mind_specif
+                ou Environ.lookup_mind_specif si on a un env sous la main
 	  mis_arity      ->  instantiate_arity
 	  mis_lc	 ->  instantiate_lc	
 
@@ -54,8 +55,8 @@ Changements dans les fonctions :
 	  gentermpr	->   gen_pr_term
 
 	Typing, Machops
-	  type_of_type     ->  type_of_sort
-	  fcn_proposition  ->  type_of_type
+	  type_of_type     ->  judge_of_type
+	  fcn_proposition  ->  judge_of_prop_contents
 
 
 Changements dans les grammaires
-- 
cgit v1.2.3