From 968d65c616127446c5f1c5d3485e9efdc420e6a4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Jul 2000 13:45:57 +0000
Subject: MAJ

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

(limited to 'dev')

diff --git a/dev/changements.txt b/dev/changements.txt
index 05d8b04f2f..e54858016c 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -75,6 +75,10 @@ Changements dans les fonctions :
 
 	Printer
 	  gentermpr	->   gen_pr_term
+          term0	        ->   prterm_env	
+          pr_sign       ->   pr_var_context
+	  pr_context_opt -> pr_context_of
+          pr_ne_env      -> pr_ne_context_of
 
 	Typing, Machops
 	  type_of_type     ->  judge_of_type
@@ -97,6 +101,7 @@ Changements dans les fonctions :
         Tacmach
           pf_constr_of_com_sort -> pf_interp_type
           pf_constr_of_com      -> pf_interp_constr
+	  pf_get_hyp            -> pf_get_hyp_typ
 
         Pattern
 	  raw_sopattern_of_compattern -> Astterm.interp_constrpattern
@@ -108,7 +113,11 @@ Changements dans les fonctions :
           dest_match            -> gl_matches
 
         Divers
-          initial_sign -> var_context
+          initial_sign     -> var_context
+
+        Sign
+          ids_of_sign      -> ids_of_var_context (or Environ.ids_of_context)
+          empty_sign       -> empty_var_context
 
         Pfedit
 	  list_proofs      -> get_all_proof_names
-- 
cgit v1.2.3