blob: 3ea6557baa025ea75e47a563809fdfbe6af961f3 (
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
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
|
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
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
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
Typing, Machops
type_of_type -> judge_of_type
fcn_proposition -> judge_of_prop_contents
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
� traduite un constr en inductive sont les find_mrectype 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*
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
|
