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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
|
MAIN CHANGES FROM COQ V7.1 TO COQ V7.2
======================================
The core of Coq (kernel) has meen minimized with the following effects:
kernel/term.ml split into kernel/term.ml, pretyping/termops.ml
kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml
kernel/names.ml split into kernel/names.ml, library/nameops.ml
kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml
the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors,
e.g. IsRel is now Rel, IsMutCase is now Case, etc.
PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0
===================================================
Changements d'organisation / modules :
--------------------------------------
Std, More_util -> lib/util.ml
Names -> kernel/names.ml et kernel/sign.ml
(les parties noms et signatures ont �t� s�par�es)
Avm,Mavm,Fmavm,Mhm -> utiliser plut�t Map (et freeze alors gratuit)
Mhb -> Bij
Generic est int�gr� � Term (et un petit peu � Closure)
Changements dans les types de donn�es :
---------------------------------------
dans Generic: free_rels : constr -> int Listset.t
devient : constr -> Intset.t
type_judgement -> typed_type
environment -> context
context -> typed_type signature
ATTENTION:
----------
Il y a maintenant d'autres exceptions que UserError (TypeError,
RefinerError, etc.)
Il ne faut donc plus se contenter (pour rattraper) de faire
try . .. with UserError _ -> ...
mais �crire � la place
try ... with e when Logic.catchable_exception e -> ...
Changements dans les fonctions :
--------------------------------
Vectops.
it_vect -> Array.fold_left
vect_it -> Array.fold_right
exists_vect -> Util.array_exists
for_all2eq_vect -> Util.array_for_all2
tabulate_vect -> Array.init
hd_vect -> Util.array_hd
tl_vect -> Util.array_tl
last_vect -> Util.array_last
it_vect_from -> array_fold_left_from
vect_it_from -> array_fold_right_from
app_tl_vect -> array_app_tl
cons_vect -> array_cons
map_i_vect -> Array.mapi
map2_vect -> array_map2
list_of_tl_vect -> array_list_of_tl
Names
sign_it -> fold_var_context (se fait sur env maintenant)
it_sign -> fold_var_context_reverse (sur env maintenant)
Generic
noccur_bet -> noccur_between
substn_many -> substnl
Std
comp -> Util.compose
rev_append -> List.rev_append
Termenv
mind_specif_of_mind -> Global.lookup_mind_specif
ou Environ.lookup_mind_specif si on a un env sous la main
mis_arity -> instantiate_arity
mis_lc -> instantiate_lc
Ex-Environ
mind_of_path -> Global.lookup_mind
Printer
gentermpr -> gen_pr_term
term0 -> prterm_env
pr_sign -> pr_var_context
pr_context_opt -> pr_context_of
pr_ne_env -> pr_ne_context_of
Typing, Machops
type_of_type -> judge_of_type
fcn_proposition -> judge_of_prop_contents
safe_fmachine -> safe_infer
Reduction, Clenv
whd_betadeltat -> whd_betaevar
whd_betadeltatiota -> whd_betaiotaevar
find_mrectype -> Inductive.find_mrectype
find_minductype -> Inductive.find_inductive
find_mcoinductype -> Inductive.find_coinductive
Astterm
constr_of_com_casted -> interp_casted_constr
constr_of_com_sort -> interp_type
constr_of_com -> interp_constr
rawconstr_of_com -> interp_rawconstr
type_of_com -> type_judgement_of_rawconstr
judgement_of_com -> judgement_of_rawconstr
Termast
bdize -> ast_of_constr
Tacmach
pf_constr_of_com_sort -> pf_interp_type
pf_constr_of_com -> pf_interp_constr
pf_get_hyp -> pf_get_hyp_typ
pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant)
Pattern
raw_sopattern_of_compattern -> Astterm.interp_constrpattern
somatch -> is_matching
dest_somatch -> matches
Tacticals
matches -> gl_is_matching
dest_match -> gl_matches
suff -> utiliser sort_of_goal
lookup_eliminator -> utiliser sort_of_goal pour le dernier arg
Divers
initial_sign -> var_context
Sign
ids_of_sign -> ids_of_var_context (or Environ.ids_of_context)
empty_sign -> empty_var_context
Pfedit
list_proofs -> get_all_proof_names
get_proof -> get_current_proof_name
abort_goal -> abort_proof
abort_goals -> abort_all_proofs
abort_cur_goal -> abort_current_proof
get_evmap_sign -> get_goal_context/get_current_goal_context
unset_undo -> reset_undo
Proof_trees
mkGOAL -> mk_goal
Declare
machine_constant -> declare_constant (+ modifs)
ex-Trad, maintenant Pretyping
inh_cast_rel -> Coercion.inh_conv_coerce_to
inh_conv_coerce_to -> Coercion.inh_conv_coerce_to_fail
ise_resolve1 -> understand, understand_type
ise_resolve -> understand_judgment, understand_type_judgment
ex-Tradevar, maintenant Evarutil
mt_tycon -> empty_tycon
Recordops
struc_info -> find_structure
Changements dans les inductifs
------------------------------
Nouveaux types "constructor" et "inductive" dans Term
La plupart des fonctions de typage des inductives prennent maintenant
un inductive au lieu d'un oonstr comme argument. Les seules fonctions
� traduire un constr en inductive sont les find_rectype and co.
Changements dans les grammaires
-------------------------------
. le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex
. attention : LIDENT -> IDENT (les identificateurs n'ont pas de
casse particuli�re dans Coq)
. Le mot "command" est remplac� par "constr" dans les noms de
fichiers, noms de modules et non-terminaux relatifs au parsing des
termes; aussi les changements suivants "COMMAND"/"CONSTR" dans
g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml*
. Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n
passent en minuscule Identifier, Constr, ...
. Plusieurs parsers ont chang� de format (ex: sortarg)
Changements dans le pretty-printing
-----------------------------------
. D�couplage de la traduction de constr -> rawconstr (dans detyping)
et de rawconstr -> ast (dans termast)
. D�placement des options d'affichage de printer vers termast
. D�placement des r�aiguillage d'univers du pp de printer vers esyntax
Changements divers
------------------
. il n'y a plus de script coqtop => coqtop et coqtop.byte sont
directement le r�sultat du link du code
=> debuggage et profiling directs
. il n'y a plus d'installation locale dans bin/$ARCH
. #use "include.ml" => #use "include"
go() => loop()
. il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
de temps
|
