blob: 2dbb9f13a7ffc82eb955e3e6d0a0026ff58ef26c (
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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
M�tath�orie
- Ajout de d�finitions locales (Let-In)
Parsing
- Le Lexeur consid�re maintenant comme token toute suite de symboles.
- "command" in grammars and quotations is now "constr" as in
pretty-printing rules
Syntaxe des constructions
- Consecutive as in patterns are forbidden
- Names generated in Cases are different (source d'incompatibilit�)
Consecutive 'as' in patterns are forbidden
- 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.
Vernac
- 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 et des
motifs des r�gles d'affichage 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), ou, si c'est dans une r�gle Syntax, utiliser la quotation
<< ... >> qui replace dans ast.
- AddPath -> Add Path;
Print LoadPath -> Print Path;
DelPath -> Remove Path;
Print Path -> Print Coercion Paths.
- Bug affichage Infix corrig�
Tactiques
- Langage de tactique
- Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial"
- Decompose :
- Num�rotation dans l'ordre des hypoth�ses cr��es
- Correction de bugs (quand le type ne commence pas par un inductif)
et refus d'agir sous les ->.
- 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�.
|
