aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/changements.txt
blob: cc5025c9c37bef40e69d20c8c880d99ddad35b5f (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
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

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