1
=========================================
2
= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
3
=========================================
5
A few differences in Coq ML interfaces between Coq V8.1 and V8.2
6
================================================================
10
List of occurrences moved from "int list" to "Termops.occurrences" (an
11
alias to "bool * int list").
15
Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply
16
Tactics: apply_with_bindings -> apply_with_bindings_wo_evars
17
Eauto.simplest_apply -> Hiddentac.h_simplest_apply
18
Evarutil.define_evar_as_arrow -> define_evar_as_product
19
Old version of Tactics.assert_tac disappears
20
Tactics.true_cut renamed into Tactics.assert_tac
21
Constrintern.interp_constrpattern -> intern_constr_pattern
22
Hipattern.match_with_conjunction is a bit more restrictive
23
Hipattern.match_with_disjunction is a bit more restrictive
25
** Universe names (univ.mli)
27
base_univ -> type0_univ (* alias of Set is the Type hierarchy *)
28
prop_univ -> type1_univ (* the type of Set in the Type hierarchy *)
29
neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *)
30
is_base_univ -> is_type1_univ
31
is_empty_univ -> is_lower_univ
33
** Sort names (term.mli)
39
=========================================
40
= CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
41
=========================================
43
A few differences in Coq ML interfaces between Coq V8.0 and V8.1
44
================================================================
48
Util: option_app -> option_map
49
Term: substl_decl -> subst_named_decl
50
Lib: library_part -> remove_section_part
51
Printer: prterm -> pr_lconstr
52
Printer: prterm_env -> pr_lconstr_env
53
Ppconstr: pr_sort -> pr_rawsort
54
Evd: in_dom, etc got standard ocaml names (i.e. mem, etc)
56
- understand_gen_tcc and understand_gen_ltac merged into understand_ltac
57
- type_constraints can now say typed by a sort (use OfType to get the
59
Library: import_library -> import_module
63
Declarations: mind_consnrealargs -> mind_consnrealdecls
65
Cast and RCast have an extra argument: you can recover the previous
66
behavior by setting the extra argument to "CastConv DEFAULTcast" and
67
"DEFAULTcast" respectively
68
Names: "kernel_name" is now "constant" when argument of Term.Const
69
Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert
70
Tacexpr: TacForward(true,_,_) branched to TacLetTac
74
module Decl_kinds: new interface
75
module Bigint: new interface
76
module Tacred spawned module Redexpr
77
module Symbols -> Notation
78
module Coqast, Ast, Esyntax, Termast, and all other modules related to old
80
module Instantiate: integrated to Evd
81
module Pretyping now a functor: use Pretyping.Default instead
85
OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE
89
- printers have an extra parameter which is a constr printer at high precedence
90
- the tactic printers have an extra arg which is the expected precedence
91
- level is now a precedence in declare_extra_tactic_pprule
92
- "interp" functions now of types the actual arg type, not its encapsulation
95
=========================================
96
= CHANGES BETWEEN COQ V7.4 AND COQ V8.0 =
97
=========================================
99
See files in dev/syntax-v8
102
==============================================
103
= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 =
104
==============================================
106
CHANGES DUE TO INTRODUCTION OF MODULES
107
======================================
112
The module level has no effect on constr except for the structure of
113
section_path. The type of unique names for constructions (what
114
section_path served) is now called a kernel name and is defined by
116
type uniq_ident = int * string * dir_path (* int may be enough *)
118
| MPfile of dir_path (* reference to physical module, e.g. file *)
119
| MPbound of uniq_ident (* reference to a module parameter in a functor *)
120
| MPself of uniq_ident (* reference to one of the containing module *)
121
| MPdot of module_path * label
122
type label = identifier
123
type kernel_name = module_path * dir_path * label
124
^^^^^^^^^^^ ^^^^^^^^ ^^^^^
128
/ the (true) section path
129
example: (non empty only inside open sections)
130
L = (* i.e. some file of logical name L *)
132
module A = struct Def a = ... end
134
M = (* i.e. some file of logical name M *)
137
N = functor (X : sig module T = struct Def b = ... end end) -> struct
141
Def x := ... <M>.t ... <N>.O.u ... X.T.b ... L.A.a
143
<M> and <N> are self-references, X is a bound reference and L is a
144
reference to a physical module.
146
Notice that functor application is not part of a path: it must be
147
named by a "module M = F(A)" declaration to be used in a kernel
150
Notice that Jacek chose a practical approach, making directories not
151
modules. Another approach could have been to replace the constructor
152
MPfile by a constant constructor MProot representing the root of the
155
Other relevant informations are in kernel/entries.ml (type
156
module_expr) and kernel/declarations.ml (type module_body and
163
[Summaries] - the only change is the special treatment of the
167
[Libobject] declares persistent objects, given with methods:
169
* cache_function specifying how to add the object in the current
171
* load_function, specifying what to do when the module
172
containing the object is loaded;
173
* open_function, specifying what to do when the module
174
containing the object is opened (imported);
175
* classify_function, specyfying what to do with the object,
176
when the current module (containing the object) is ended.
178
* export_function, to signal end_section survival
180
(Almost) Each of these methods is called with a parameter of type
181
object_name = section_path * kernel_name
182
where section_path is the full user name of the object (such as
183
Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal
184
version such as (MPself<Datatypes#1>,[],"Fst") (see above)
187
What happens at the end of an interactive module ?
188
==================================================
189
(or when a file is stored and reloaded from disk)
191
All summaries (except Global environment) are reverted to the state
192
from before the beginning of the module, and:
194
a) the objects (again, since last Declaremods.start_module or
195
Library.start_library) are classified using the classify_function.
196
To simplify consider only those who returned Substitute _ or Keep _.
198
b) If the module is not a functor, the subst_function for each object of
199
the first group is called with the substitution
200
[MPself "<Datatypes#1>" |-> MPfile "Coq.Init.Datatypes"].
201
Then the load_function is called for substituted objects and the
203
(If the module is a library the substitution is done at reloading).
205
c) The objects which returned substitute are stored in the modtab
206
together with the self ident of the module, and functor argument
207
names if the module was a functor.
209
They will be used (substituted and loaded) when a command like
215
The difference between "substitute" and "keep" objects
216
========================================================
217
i) The "keep" objects can _only_ reference other objects by section_paths
218
and qualids. They do not need the substitution function.
220
They will work after end_module (or reloading a compiled library),
221
because these operations do not change section_path's
223
They will obviously not work after Module Z:=N.
225
These would typically be grammar rules, pretty printing rules etc.
229
ii) The "substitute" objects can _only_ reference objects by
230
kernel_names. They must have a valid subst_function.
232
They will work after end_module _and_ after Module Z:=N or
237
Other kinds of objects:
238
iii) "Dispose" - objects which do not survive end_module
239
As a consequence, objects which reference other objects sometimes
240
by kernel_names and sometimes by section_path must be of this kind...
242
iv) "Anticipate" - objects which must be treated individually by
243
end_module (typically "REQUIRE" objects)
247
Writing subst_thing functions
248
=============================
249
The subst_thing shoud not copy the thing if it hasn't actually
250
changed. There are some cool emacs macros in dev/objects.el
251
to help writing subst functions this way quickly and without errors.
252
Also there are *_smartmap functions in Util.
254
The subst_thing functions are already written for many types,
255
including constr (Term.subst_mps),
256
global_reference (Libnames.subst_global),
257
rawconstr (Rawterm.subst_raw) etc
259
They are all (apart from constr, for now) written in the non-copying
266
Nametab has been made more uniform. For every kind of thing there is
267
only one "push" function and one "locate" function.
273
library_segment is now a list of object_name * library_item, where
274
object_name = section_path * kernel_name (see above)
276
New items have been added for open modules and module types
281
Functions to declare interactive and noninteractive modules and module
287
Uses Declaremods to actually communicate with Global and to register
294
Internal representation of tactics bindings has changed (see type
295
Rawterm.substitution).
297
New parsing model for tactics and vernacular commands
299
- Introduction of a dedicated type for tactic expressions
300
(Tacexpr.raw_tactic_expr)
301
- Introduction of a dedicated type for vernac expressions
302
(Vernacexpr.vernac_expr)
303
- Declaration of new vernacular parsing rules by a new camlp4 macro
304
GRAMMAR COMMAND EXTEND ... END to be used in ML files
305
- Declaration of new tactics parsing/printing rules by a new camlp4 macro
306
TACTIC EXTEND ... END to be used in ML files
308
New organisation of THENS:
309
tclTHENS tac tacs : tacs is now an array
310
tclTHENSFIRSTn tac1 tacs tac2 :
311
apply tac1 then, apply the array tacs on the first n subgoals and
312
tac2 on the remaining subgoals (previously tclTHENST)
313
tclTHENSLASTn tac1 tac2 tacs :
314
apply tac1 then, apply tac2 on the first subgoals and apply the array
315
tacs on the last n subgoals
316
tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI)
317
tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs
318
tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|]
319
tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL)
320
tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number")
321
tclTHENSV same as tclTHENS but with an array
322
tclTHENSi : no longer available
324
Proof_type: subproof field in type proof_tree glued with the ref field
326
Tacmach: no more echo from functions of module Refiner
328
Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v.
329
Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd
330
VERNAC COMMAND EXTEND macros
331
File syntax/PPTactic.v moved to parsing/pptactic.ml
332
Tactics about False and not now in tactics/contradiction.ml
333
Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v)
334
File tacinterp.ml moved from proofs to directory tactics
337
==========================================
338
= MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 =
339
==========================================
341
The core of Coq (kernel) has meen minimized with the following effects:
343
kernel/term.ml split into kernel/term.ml, pretyping/termops.ml
344
kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml
345
kernel/names.ml split into kernel/names.ml, library/nameops.ml
346
kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml
348
the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors,
349
e.g. IsRel is now Rel, IsMutCase is now Case, etc.
352
=======================================================
353
= PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0 =
354
=======================================================
356
Changements d'organisation / modules :
357
--------------------------------------
359
Std, More_util -> lib/util.ml
361
Names -> kernel/names.ml et kernel/sign.ml
362
(les parties noms et signatures ont �t� s�par�es)
364
Avm,Mavm,Fmavm,Mhm -> utiliser plut�t Map (et freeze alors gratuit)
367
Generic est int�gr� � Term (et un petit peu � Closure)
369
Changements dans les types de donn�es :
370
---------------------------------------
371
dans Generic: free_rels : constr -> int Listset.t
372
devient : constr -> Intset.t
374
type_judgement -> typed_type
375
environment -> context
376
context -> typed_type signature
382
Il y a maintenant d'autres exceptions que UserError (TypeError,
385
Il ne faut donc plus se contenter (pour rattraper) de faire
387
try . .. with UserError _ -> ...
389
mais �crire � la place
391
try ... with e when Logic.catchable_exception e -> ...
394
Changements dans les fonctions :
395
--------------------------------
398
it_vect -> Array.fold_left
399
vect_it -> Array.fold_right
400
exists_vect -> Util.array_exists
401
for_all2eq_vect -> Util.array_for_all2
402
tabulate_vect -> Array.init
403
hd_vect -> Util.array_hd
404
tl_vect -> Util.array_tl
405
last_vect -> Util.array_last
406
it_vect_from -> array_fold_left_from
407
vect_it_from -> array_fold_right_from
408
app_tl_vect -> array_app_tl
409
cons_vect -> array_cons
410
map_i_vect -> Array.mapi
411
map2_vect -> array_map2
412
list_of_tl_vect -> array_list_of_tl
415
sign_it -> fold_var_context (se fait sur env maintenant)
416
it_sign -> fold_var_context_reverse (sur env maintenant)
419
noccur_bet -> noccur_between
420
substn_many -> substnl
424
rev_append -> List.rev_append
427
mind_specif_of_mind -> Global.lookup_mind_specif
428
ou Environ.lookup_mind_specif si on a un env sous la main
429
mis_arity -> instantiate_arity
430
mis_lc -> instantiate_lc
433
mind_of_path -> Global.lookup_mind
436
gentermpr -> gen_pr_term
438
pr_sign -> pr_var_context
439
pr_context_opt -> pr_context_of
440
pr_ne_env -> pr_ne_context_of
443
type_of_type -> judge_of_type
444
fcn_proposition -> judge_of_prop_contents
445
safe_fmachine -> safe_infer
448
whd_betadeltat -> whd_betaevar
449
whd_betadeltatiota -> whd_betaiotaevar
450
find_mrectype -> Inductive.find_mrectype
451
find_minductype -> Inductive.find_inductive
452
find_mcoinductype -> Inductive.find_coinductive
455
constr_of_com_casted -> interp_casted_constr
456
constr_of_com_sort -> interp_type
457
constr_of_com -> interp_constr
458
rawconstr_of_com -> interp_rawconstr
459
type_of_com -> type_judgement_of_rawconstr
460
judgement_of_com -> judgement_of_rawconstr
463
bdize -> ast_of_constr
466
pf_constr_of_com_sort -> pf_interp_type
467
pf_constr_of_com -> pf_interp_constr
468
pf_get_hyp -> pf_get_hyp_typ
469
pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant)
472
raw_sopattern_of_compattern -> Astterm.interp_constrpattern
473
somatch -> is_matching
474
dest_somatch -> matches
477
matches -> gl_is_matching
478
dest_match -> gl_matches
479
suff -> utiliser sort_of_goal
480
lookup_eliminator -> utiliser sort_of_goal pour le dernier arg
483
initial_sign -> var_context
486
ids_of_sign -> ids_of_var_context (or Environ.ids_of_context)
487
empty_sign -> empty_var_context
490
list_proofs -> get_all_proof_names
491
get_proof -> get_current_proof_name
492
abort_goal -> abort_proof
493
abort_goals -> abort_all_proofs
494
abort_cur_goal -> abort_current_proof
495
get_evmap_sign -> get_goal_context/get_current_goal_context
496
unset_undo -> reset_undo
502
machine_constant -> declare_constant (+ modifs)
504
ex-Trad, maintenant Pretyping
505
inh_cast_rel -> Coercion.inh_conv_coerce_to
506
inh_conv_coerce_to -> Coercion.inh_conv_coerce_to_fail
507
ise_resolve1 -> understand, understand_type
508
ise_resolve -> understand_judgment, understand_type_judgment
510
ex-Tradevar, maintenant Evarutil
511
mt_tycon -> empty_tycon
514
struc_info -> find_structure
516
Changements dans les inductifs
517
------------------------------
518
Nouveaux types "constructor" et "inductive" dans Term
519
La plupart des fonctions de typage des inductives prennent maintenant
520
un inductive au lieu d'un oonstr comme argument. Les seules fonctions
521
� traduire un constr en inductive sont les find_rectype and co.
523
Changements dans les grammaires
524
-------------------------------
526
. le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex
528
. attention : LIDENT -> IDENT (les identificateurs n'ont pas de
529
casse particuli�re dans Coq)
531
. Le mot "command" est remplac� par "constr" dans les noms de
532
fichiers, noms de modules et non-terminaux relatifs au parsing des
533
termes; aussi les changements suivants "COMMAND"/"CONSTR" dans
534
g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml*
536
. Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n
537
passent en minuscule Identifier, Constr, ...
539
. Plusieurs parsers ont chang� de format (ex: sortarg)
541
Changements dans le pretty-printing
542
-----------------------------------
544
. D�couplage de la traduction de constr -> rawconstr (dans detyping)
545
et de rawconstr -> ast (dans termast)
546
. D�placement des options d'affichage de printer vers termast
547
. D�placement des r�aiguillage d'univers du pp de printer vers esyntax
553
. il n'y a plus de script coqtop => coqtop et coqtop.byte sont
554
directement le r�sultat du link du code
555
=> debuggage et profiling directs
557
. il n'y a plus d'installation locale dans bin/$ARCH
559
. #use "include.ml" => #use "include"
562
. il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup
added
removed
dev/doc/changes.txt
