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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
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 "?".
- Davantage d'arguments implicites engendr�s par le discharge.
- 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
"ast list"), ou, si c'est dans une r�gle Syntax, utiliser la quotation
<< ... >> qui replace dans ast. Pour les nouvelles grammaires (autre
que les 3 primitives), on peut typer avec "constr", "tactic", ou
"vernac" pour utiliser le parseur correspondant.
- AddPath -> Add Path;
Print LoadPath -> Print Path;
DelPath -> Remove Path;
Print Path -> Print Coercion Paths.
- Bug affichage Infix corrig�
- L�g�re restriction de la syntaxe de Cbv Delta
- L'option [-myconst] de Cbv doit imm�diatement suivre Delta
- End Silent etait interprete comme une fin de section
Begin Silent -> Set Silent
End Silent -> Unset Silent.
- D�claration manuelle des implicites avec
Implicits ident.
Implicits ident [ num num ... num ].
Petit changement de s�mantique : lors de la fermeture d'une section,
les implicites sont calcul�s selon la valeur *courante* de "Implicit
Arguments" et non plus selon la valeur qu'elle avait au moment de la
d�finition dans la section.
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�.
- EAuto r�ussit parfois plus (source d'incompatibilit�).
- Intro �choue si le nom d'hypoth�se existe au lieu de mettre un avertissement
Outils
- deux binaires maximum : coqtop.byte et coqtop.opt si plateforme native;
coqtop est un lien vers le plus efficace possible (coqtop.opt s'il existe,
coqtop.byte sinon); -full maintenant obsolete
- do_Makefile s'appelle maintenant coq_makefile
Utilisation g�n�rale
- La plupart des erreurs de typage sont maintenant localis�e dans le
source (� l'exception des erreurs d'univers et de garde).
- Rapidit� accrue
D�veloppeurs
- Beaucoup de modification dans le sens de la simplification et de la
documentation (mais cela reste une version de transition)
|
