From 90a4f633cb322804969202ef96cd1ac3f8863f2b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 5 May 2000 13:29:54 +0000
Subject: MAJ

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

(limited to 'dev')

diff --git a/dev/changements.txt b/dev/changements.txt
index 8d028c2359..918d1d40f8 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -107,11 +107,19 @@ Changements dans les fonctions :
           initial_sign -> var_context
 
         Pfedit
-	  list_proofs -> get_all_proof_names
-          get_proof -> get_current_proof_name
-          abort_cur_goal -> abort_current_goal
-          get_evmap_sign -> get_goal_context/get_current_goal_context
-          unset_undo -> reset_undo
+	  list_proofs      -> get_all_proof_names
+          get_proof        -> get_current_proof_name
+          abort_goal       -> abort_proof
+          abort_goals      -> abort_all_proofs
+          abort_cur_goal   -> abort_current_proof
+          get_evmap_sign   -> get_goal_context/get_current_goal_context
+          unset_undo       -> reset_undo
+
+        Proof_trees
+          mkGOAL           -> mk_goal
+
+        Declare
+  	  machine_constant ->   declare_constant (+ modifs)
 
 Changements dans les inductifs
 ------------------------------
@@ -133,7 +141,10 @@ Changements dans les grammaires
  termes; aussi les changements suivants "COMMAND"/"CONSTR" dans
  g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml*
 
+ . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n
+   passent en minuscule Identifier, Constr, ...
  
+ . Plusieurs parsers ont changé de format (ex: sortarg)
 
 Changements dans le pretty-printing
 -----------------------------------
-- 
cgit v1.2.3