aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/changements.txt8
1 files changed, 8 insertions, 0 deletions
diff --git a/dev/changements.txt b/dev/changements.txt
index 918d1d40f8..05d8b04f2f 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -56,6 +56,10 @@ Changements dans les fonctions :
map2_vect -> array_map2
list_of_tl_vect -> array_list_of_tl
+ Generic
+ noccur_bet -> noccur_between
+ substn_many -> substnl
+
Std
comp -> Util.compose
rev_append -> List.rev_append
@@ -121,6 +125,10 @@ Changements dans les fonctions :
Declare
machine_constant -> declare_constant (+ modifs)
+ ex-Trad
+ inh_cast_rel -> Coercion.inh_conv_coerce_to
+ inh_conv_coerce_to -> Coercion.inh_conv_coerce_to_fail
+
Changements dans les inductifs
------------------------------
Nouveaux types "constructor" et "inductive" dans Term