blob: 08802e0533d5174a4a1a7ab2dc861e78ea81d856 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
- 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. En
revanche, si une constante n'est qu'indirectement un Fix, on ne garde
en g�n�ral plus son nom (sauf dans les cas "simples"). Rem : c'est une
source d'incompatibilit�.
- Davantage d'inf�rence automatique de "?".
- 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.
- Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des
phrases (utile pour Time et pour des grammaires abr�geant plusieurs
commandes)
- Le parseur par d�faut des actions des r�gles de grammaires est
maintenant celui associ� au nom de la grammaire (vernac, tactic ou
constr). Donc plus de piquants <:vernac:<...>> etc. Pour retourner de
l'ast, il faut typer explicitement la grammaire avec Ast ou List
(renomm� d'ailleurs AstList).
- AddPath -> Add Path;
Print LoadPath -> Print Path;
DelPath -> Remove Path;
Print Path -> Print Coercion Paths.
- Ajout d'un Let primitif
- Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial"
- Langage de tactique
|
