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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
M�tath�orie
- Ajout de d�finitions locales (Let-In) avec la syntaxe [x:=u]t. Cela
peut entrainer des comportements nouveaux pour certaines tactiques.
- Les d�finitions globales de la biblioth�que standard sont associ�es
� un nom long refl�tant la structure logique de la notion. Un tel nom
long a la forme Coq.Lists.PolyList.Map.flat_map o� Coq d�note que la
d�finition flat_map fait partie de la biblioth�que standard, Lists
qu'elle se trouve dans le r�pertoire Lists, PolyList qu'elle se trouve
dans le module PolyList, et Map qu'elle se trouve dans la section Map.
- On peut (et il est conseill�) associer � un r�pertoire physique un
nom logique dans la structure des noms de Coq. Les d�finitions de la
biblioth�que standard sont associ�es au pr�fixe logique `Coq'. Pour
associer un r�pertoire physique � un nom logique, il faut utiliser
l'option -R de coqtop et coqc (cf Outils). Par d�faut, le nom logique
"Scratch" est utilis� pour toute d�finition globale non associ�e � un
module non associ� � un nom logique.
Parsing
- Le Lexeur consid�re maintenant comme token toute suite de symboles
(source d'incompatibilit� : il faut ins�rer des espaces entre tokens
sp�ciaux cons�cutifs)
- "command" in grammars and quotations is now "constr" as in
pretty-printing rules
Syntaxe des constructions
- Le nom long des d�finitions globales est accessible pour
l'utilisateur par la notation point�e (style Coq.Arith.Plus.plus_assoc_l).
La syntaxe du "." final change (cf Vernac). Le nommage des d�finitions
globales change (cf M�tath�orie).
- 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.
- Les d�clarations de constantes et de variables peuvent maintenant
�tre acc�d�es par un nom long de la forme "Logic.f_equal". La
biblioth�que standard a maintenant une racine nomm�e "Coq". Tout nom
de la forme "Coq.Logic.f_equal" d�note ainsi un chemin absolu vers une
d�claration.
Syntaxe des theories
- Ajout d'une syntaxe pour les reels: ``Rexpr``.
Point noir du aux constantes:
(Rplus (Rplus (Rplus R1 R1) (Rplus R1 R1)) R1) est toujours (2+2+1)
au lieu de 2+2+1
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 piqants
<: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.
- SearchPattern / SearchRewrite (contrib de Yves Bertot)
- Le point final des commandes doit �tre suivi d'un blanc (retour chariot, tabulation ou espace)
Tactiques
- Langage de tactique Ltac
- 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�.
- Intro �choue si le nom d'hypoth�se existe au lieu de mettre un avertissement
- Plus de "Require Prolog" (int�gr� par d�faut)
- Unfold �choue si on lui donne en argument une d�finition non d�pliable
- AutoRewrite ne s'occupe maintenant que du but principal et c'est les
Hint Rewrite qui g�rent les sous-buts g�n�r�s
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 de l'option -R de coqtop et coqc pour associer un
g r�pertoire physique � un r�pertoire logique (cf M�tath�orie)
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)
|
