aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
blob: 537592357093175bd390b7f644381aaa61bee558 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
- Consecutive as in patterns are forbidden

- Names generated in Cases are different

- "command" in grammars is now "constr" as in pretty-printing rules

- Num�rotation dans l'ordre des hypoth�ses cr��es par Decompose
- Correction de bugs (quand le type ne commence pas par un inductif)

- Simpl ne d�plie plus les appels r�cursifs d'un Fix mutuel r�duit

- Les cas des Cases ne se lisent plus de mani�re s�quentielle, sauf en
  cas de clauses par d�faut redondantes auquel cas la premi�re est prise
  avec un avertissement.