From c5ebef7a746564f8ac41c19d5ac9ca64f60dcf4a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Sep 2000 16:47:31 +0000
Subject: MAJ

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

(limited to 'dev')

diff --git a/dev/changements.txt b/dev/changements.txt
index e6d44eb45a..7aeda57a7b 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -140,8 +140,8 @@ Changements dans les fonctions :
 	ex-Trad, maintenant Pretyping
           inh_cast_rel        -> Coercion.inh_conv_coerce_to
           inh_conv_coerce_to  -> Coercion.inh_conv_coerce_to_fail
-	  ise_resolve1        -> ise_resolve, ise_resolve_type
-	  ise_resolve         -> ise_infer, ise_infer_type
+	  ise_resolve1        -> understand, understand_type
+	  ise_resolve         -> understand_judgment, understand_type_judgment
 
 Changements dans les inductifs
 ------------------------------
-- 
cgit v1.2.3