blob: 538424d7fc0f5b64e203fe77821e16b5385f2dce (
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
|
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
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_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 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)
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/
. #use "include.ml" => #use "include"
go() => loop()
. il y "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
de temps
|
