aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/changements.txt3
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/changements.txt b/dev/changements.txt
index f94e534560..00bfa46637 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -153,6 +153,9 @@ Changements dans les fonctions :
ise_resolve1 -> understand, understand_type
ise_resolve -> understand_judgment, understand_type_judgment
+ ex-Tradevar, maintenant Evarutil
+ mt_tycon -> empty_tycon
+
Changements dans les inductifs
------------------------------
Nouveaux types "constructor" et "inductive" dans Term