From d75ed9715818820511704beaa2bb6c7acf1b1aba Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 28 Apr 2000 19:25:22 +0000
Subject: MAJ

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

(limited to 'dev')

diff --git a/dev/changements.txt b/dev/changements.txt
index 6293de2960..ca07f799c9 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -87,10 +87,20 @@ Changements dans les fonctions :
           rawconstr_of_com     -> interp_rawconstr
           type_of_com          -> typed_type_of_com
 
+        Termast
+          bdize                -> ast_of_constr
+
         Tacmach
           pf_constr_of_com_sort -> pf_interp_type
           pf_constr_of_com      -> pf_interp_constr
 
+        Pattern
+	  somatch               -> is_matching
+          dest_somatch          -> matches
+
+        Tacticals
+	  matches               -> gl_is_matching
+          dest_match            -> gl_matches
 
 Changements dans les inductifs
 ------------------------------
-- 
cgit v1.2.3