diff options
Diffstat (limited to 'dev/doc/changes.txt')
-rw-r--r-- | dev/doc/changes.txt | 1095 |
1 files changed, 0 insertions, 1095 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt deleted file mode 100644 index 3de938d7..00000000 --- a/dev/doc/changes.txt +++ /dev/null @@ -1,1095 +0,0 @@ -========================================= -= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = -========================================= - -** Parsing ** - -Pcoq.parsable now takes an extra optional filename argument so as to -bind locations to a file name when relevant. - -** Files ** - -To avoid clashes with OCaml's compiler libs, the following files were renamed: -kernel/closure.ml{,i} -> kernel/cClosure.ml{,i} -lib/errors.ml{,i} -> lib/cErrors.ml{,i} -toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i} - -All IDE-specific files, including the XML protocol have been moved to ide/ - -** Reduction functions ** - -In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX, -fCOFIX. - -We renamed the following functions: - -Closure.betadeltaiota -> Closure.all -Closure.betadeltaiotanolet -> Closure.allnolet -Reductionops.beta -> Closure.beta -Reductionops.zeta -> Closure.zeta -Reductionops.betaiota -> Closure.betaiota -Reductionops.betaiotazeta -> Closure.betaiotazeta -Reductionops.delta -> Closure.delta -Reductionops.betalet -> Closure.betazeta -Reductionops.betadelta -> Closure.betadeltazeta -Reductionops.betadeltaiota -> Closure.all -Reductionops.betadeltaiotanolet -> Closure.allnolet -Closure.no_red -> Closure.nored -Reductionops.nored -> Closure.nored -Reductionops.nf_betadeltaiota -> Reductionops.nf_all -Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta -Reductionops.whd_betadeltaiota -> Reductionops.whd_all -Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet -Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack -Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack -Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack -Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state -Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state -Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state -Reductionops.whd_eta -> Reductionops.shrink_eta -Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all -Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all - -And removed the following ones: - -Reductionops.whd_betaetalet -Reductionops.whd_betaetalet_stack -Reductionops.whd_betaetalet_state -Reductionops.whd_betadeltaeta_stack -Reductionops.whd_betadeltaeta_state -Reductionops.whd_betadeltaeta -Reductionops.whd_betadeltaiotaeta_stack -Reductionops.whd_betadeltaiotaeta_state -Reductionops.whd_betadeltaiotaeta - -In intf/genredexpr.mli, fIota was replaced by FMatch, FFix and -FCofix. Similarly, rIota was replaced by rMatch, rFix and rCofix. - -** Notation_ops ** - -Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. - -** Logging and Pretty Printing: ** - -* Printing functions have been removed from `Pp.mli`, which is now a - purely pretty-printing interface. Functions affected are: - -```` ocaml -val pp : std_ppcmds -> unit -val ppnl : std_ppcmds -> unit -val pperr : std_ppcmds -> unit -val pperrnl : std_ppcmds -> unit -val pperr_flush : unit -> unit -val pp_flush : unit -> unit -val flush_all : unit -> unit -val msg : std_ppcmds -> unit -val msgnl : std_ppcmds -> unit -val msgerr : std_ppcmds -> unit -val msgerrnl : std_ppcmds -> unit -val message : string -> unit -```` - - which are no more available. Users of `Pp.pp msg` should now use the - proper `Feedback.msg_*` function. Clients also have no control over - flushing, the back end takes care of it. - - Also, the `msg_*` functions now take an optional `?loc` parameter - for relaying location to the client. - -* Feedback related functions and definitions have been moved to the - `Feedback` module. `message_level` has been renamed to - level. Functions moved from Pp to Feedback are: - -```` ocaml -val set_logger : logger -> unit -val std_logger : logger -val emacs_logger : logger -val feedback_logger : logger -```` - -* Changes in the Feedback format/Protocol. - -- The `Message` feedback type now carries an optional location, the main - payload is encoded using the richpp document format. - -- The `ErrorMsg` feedback type is thus unified now with `Message` at - level `Error`. - -* We now provide several loggers, `log_via_feedback` is removed in - favor of `set_logger feedback_logger`. Output functions are: - -```` ocaml -val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b -val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit -val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit -val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit -val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit -val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit -```` - - with the `msg_*` functions being just an alias for `logger $Level`. - -* The main feedback functions are: - -```` ocaml -val set_feeder : (feedback -> unit) -> unit -val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit -val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit -```` - Note that `feedback` doesn't take two parameters anymore. After - refactoring the following function has been removed: - -```` ocaml -val get_id_for_feedback : unit -> edit_or_state_id * route_id -```` - -** Kernel API changes ** - -- The interface of the Context module was changed. - Related types and functions were put in separate submodules. - The mapping from old identifiers to new identifiers is the following: - - Context.named_declaration ---> Context.Named.Declaration.t - Context.named_list_declaration ---> Context.NamedList.Declaration.t - Context.rel_declaration ---> Context.Rel.Declaration.t - Context.map_named_declaration ---> Context.Named.Declaration.map_constr - Context.map_named_list_declaration ---> Context.NamedList.Declaration.map - Context.map_rel_declaration ---> Context.Rel.Declaration.map_constr - Context.fold_named_declaration ---> Context.Named.Declaration.fold - Context.fold_rel_declaration ---> Context.Rel.Declaration.fold - Context.exists_named_declaration ---> Context.Named.Declaration.exists - Context.exists_rel_declaration ---> Context.Rel.Declaration.exists - Context.for_all_named_declaration ---> Context.Named.Declaration.for_all - Context.for_all_rel_declaration ---> Context.Rel.Declaration.for_all - Context.eq_named_declaration ---> Context.Named.Declaration.equal - Context.eq_rel_declaration ---> Context.Rel.Declaration.equal - Context.named_context ---> Context.Named.t - Context.named_list_context ---> Context.NamedList.t - Context.rel_context ---> Context.Rel.t - Context.empty_named_context ---> Context.Named.empty - Context.add_named_decl ---> Context.Named.add - Context.vars_of_named_context ---> Context.Named.to_vars - Context.lookup_named ---> Context.Named.lookup - Context.named_context_length ---> Context.Named.length - Context.named_context_equal ---> Context.Named.equal - Context.fold_named_context ---> Context.Named.fold_outside - Context.fold_named_list_context ---> Context.NamedList.fold - Context.fold_named_context_reverse ---> Context.Named.fold_inside - Context.instance_from_named_context ---> Context.Named.to_instance - Context.extended_rel_list ---> Context.Rel.to_extended_list - Context.extended_rel_vect ---> Context.Rel.to_extended_vect - Context.fold_rel_context ---> Context.Rel.fold_outside - Context.fold_rel_context_reverse ---> Context.Rel.fold_inside - Context.map_rel_context ---> Context.Rel.map_constr - Context.map_named_context ---> Context.Named.map_constr - Context.iter_rel_context ---> Context.Rel.iter - Context.iter_named_context ---> Context.Named.iter - Context.empty_rel_context ---> Context.Rel.empty - Context.add_rel_decl ---> Context.Rel.add - Context.lookup_rel ---> Context.Rel.lookup - Context.rel_context_length ---> Context.Rel.length - Context.rel_context_nhyps ---> Context.Rel.nhyps - Context.rel_context_tags ---> Context.Rel.to_tags - -- Originally, rel-context was represented as: - - Context.rel_context = Names.Name.t * Constr.t option * Constr.t - - Now it is represented as: - - Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t - | LocalDef of Names.Name.t * Constr.t * Constr.t - -- Originally, named-context was represented as: - - Context.named_context = Names.Id.t * Constr.t option * Constr.t - - Now it is represented as: - - Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t - | LocalDef of Names.Id.t * Constr.t * Constr.t - -- The various EXTEND macros do not handle specially the Coq-defined entries - anymore. Instead, they just output a name that have to exist in the scope - of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for - variables "$name" of type Gram.entry, while the parsing rules of - (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will - look for variables "wit_$name" of type Genarg.genarg_type. The small DSL - for constructing compound entries still works over this scheme. Note that in - the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound - in the parsing rules, so beware of recursive calls. - - For example, to get "wit_constr" you must "open Constrarg" at the top of the file. - -- Evarutil was split in two parts. The new Evardefine file exposes functions -define_evar_* mostly used internally in the unification engine. - -- The Refine module was move out of Proofview. - - Proofview.Refine.* ---> Refine.* - -- A statically monotonous evarmap type was introduced in Sigma. Not all the API - has been converted, so that the user may want to use compatibility functions - Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when - needed. Code can be straightforwardly adapted in the following way: - - let (sigma, x1) = ... in - ... - let (sigma, xn) = ... in - (sigma, ans) - - should be turned into: - - open Sigma.Notations - - let Sigma (x1, sigma, p1) = ... in - ... - let Sigma (xn, sigma, pn) = ... in - Sigma (ans, sigma, p1 +> ... +> pn) - - Examples of `Sigma.Unsafe.of_evar_map` include: - - Evarutil.new_evar env (Tacmach.project goal) ty ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty - -- The Proofview.Goal.*enter family of functions now takes a polymorphic - continuation given as a record as an argument. - - Proofview.Goal.enter begin fun gl -> ... end - - should be turned into - - open Proofview.Notations - - Proofview.Goal.enter { enter = begin fun gl -> ... end } - -- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` -- `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)` -- `Pretyping.Termops.mem_named_context` ---> `Engine.Termops.mem_named_context_val` - (`Global.named_context` ---> `Global.named_context_val`) - (`Context.Named.lookup` ---> `Environ.lookup_named_val`) - -** Search API ** - -The main search functions now take a function iterating over the -results. This allows for clients to use streaming or more economic -printing. - -========================================= -= CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = -========================================= - -** Refactoring : more mli interfaces and simpler grammar.cma ** - -- A new directory intf/ now contains mli-only interfaces : - - Constrexpr : definition of constr_expr, was in Topconstr - Decl_kinds : now contains binding_kind = Explicit | Implicit - Evar_kinds : type Evar_kinds.t was previously Evd.hole_kind - Extend : was parsing/extend.mli - Genredexpr : regroup Glob_term.red_expr_gen and Tacexpr.glob_red_flag - Glob_term : definition of glob_constr - Locus : definition of occurrences and stuff about clauses - Misctypes : intro_pattern_expr, glob_sort, cast_type, or_var, ... - Notation_term : contains notation_constr, was Topconstr.aconstr - Pattern : contains constr_pattern - Tacexpr : was tactics/tacexpr.ml - Vernacexpr : was toplevel/vernacexpr.ml - -- Many files have been divided : - - vernacexpr: vernacexpr.mli + Locality - decl_kinds: decl_kinds.mli + Kindops - evd: evar_kinds.mli + evd - tacexpr: tacexpr.mli + tacops - glob_term: glob_term.mli + glob_ops + genredexpr.mli + redops - topconstr: constrexpr.mli + constrexpr_ops - + notation_expr.mli + notation_ops + topconstr - pattern: pattern.mli + patternops - libnames: libnames (qualid, reference) + globnames (global_reference) - egrammar: egramml + egramcoq - -- New utility files : miscops (cf. misctypes.mli) and - redops (cf genredexpr.mli). - -- Some other directory changes : - * grammar.cma and the source files specific to it are now in grammar/ - * pretty-printing files are now in printing/ - -- Inner-file changes : - - * aconstr is now notation_constr, all constructors for this type - now start with a N instead of a A (e.g. NApp instead of AApp), - and functions about aconstr may have been renamed (e.g. match_aconstr - is now match_notation_constr). - - * occurrences (now in Locus.mli) is now an algebraic type, with - - AllOccurrences instead of all_occurrences_expr = (false,[]) - - (AllOccurrencesBut l) instead of (all_occurrences_expr_but l) = (false,l) - - NoOccurrences instead of no_occurrences_expr = (true,[]) - - (OnlyOccurrences l) instead of (no_occurrences_expr_but l) = (true,l) - - * move_location (now in Misctypes) has two new constructors - MoveFirst and MoveLast replacing (MoveToEnd false) and (MoveToEnd true) - -- API of pretyping.ml and constrintern.ml has been made more uniform - * Parametrization of understand_* functions is now made using - "inference flags" - * Functions removed: - - interp_constr_judgment (inline its former body if really needed) - - interp_casted_constr, interp_type: use instead interp_constr with - expected_type set to OfType or to IsType - - interp_gen: use any of interp_constr, interp_casted_constr, interp_type - - interp_open_constr_patvar - - interp_context: use interp_context_evars (with a "evar_map ref") and - call solve_remaining_evars afterwards with a failing flag - (e.g. all_and_fail_flags) - - understand_type, understand_gen: use understand with appropriate - parameters - * Change of semantics: - - Functions interp_*_evars_impls have a different interface and do - not any longer check resolution of evars by default; use - check_evars_are_solved explicitly to check that evars are solved. - See also the corresponding commit log. - -- Tactics API: new_induct -> induction; new_destruct -> destruct; - letin_pat_tac do not accept a type anymore - -- New file find_subterm.ml for gathering former functions - subst_closed_term_occ_modulo, subst_closed_term_occ_decl (which now - take and outputs also an evar_map), and - subst_closed_term_occ_modulo, subst_closed_term_occ_decl_modulo (now - renamed into replace_term_occ_modulo and - replace_term_occ_decl_modulo). - -- API of Inductiveops made more uniform (see commit log or file itself). - -- API of intros_pattern style tactic changed; "s" is dropped in - "intros_pattern" and "intros_patterns" is not anymore behaving like - tactic "intros" on the empty list. - -- API of cut tactics changed: for instance, cut_intro should be replaced by - "assert_after Anonymous" - -- All functions taking an env and a sigma (or an evdref) now takes the - env first. - -========================================= -= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = -========================================= - -** Functions in unification.ml have now the evar_map coming just after the env - -** Removal of Tacinterp.constr_of_id ** - -Use instead either global_reference or construct_reference in constrintern.ml. - -** Optimizing calls to Evd functions ** - -Evars are split into defined evars and undefined evars; for -efficiency, when an evar is known to be undefined, it is preferable to -use specific functions about undefined evars since these ones are -generally fewer than the defined ones. - -** Type changes in TACTIC EXTEND rules ** - -Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type -glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first -component is kept, the second one can be obtained via -Tacinterp.eval_tactic. - -** ARGUMENT EXTEND ** - -It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED -in ARGUMENT EXTEND statements. - -** Renaming of rawconstr to glob_constr ** - -The "rawconstr" type has been renamed to "glob_constr" for -consistency. The "raw" in everything related to former rawconstr has -been changed to "glob". For more details about the rationale and -scripts to migrate code using Coq's internals, see commits 13743, -13744, 13755, 13756, 13757, 13758, 13761 (by glondu, end of December -2010) in Subversion repository. Contribs have been fixed too, and -commit messages there might also be helpful for migrating. - -========================================= -= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = -========================================= - -** Light cleaning in evarutil.ml ** - -whd_castappevar is now whd_head_evar -obsolete whd_ise disappears - -** Restructuration of the syntax of binders ** - -binders_let -> binders -binders_let_fixannot -> binders_fixannot -binder_let -> closed_binder (and now covers only bracketed binders) -binder was already obsolete and has been removed - -** Semantical change of h_induction_destruct ** - -Warning, the order of the isrec and evar_flag was inconsistent and has -been permuted. Tactic induction_destruct in tactics.ml is unchanged. - -** Internal tactics renamed - -There is no more difference between bindings and ebindings. The -following tactics are therefore renamed - -apply_with_ebindings_gen -> apply_with_bindings_gen -left_with_ebindings -> left_with_bindings -right_with_ebindings -> right_with_bindings -split_with_ebindings -> split_with_bindings - -and the following tactics are removed - -apply_with_ebindings (use instead apply_with_bindings) -eapply_with_ebindings (use instead eapply_with_bindings) - -** Obsolete functions in typing.ml - -For mtype_of, msort_of, mcheck, now use type_of, sort_of, check - -** Renaming functions renamed - -concrete_name -> compute_displayed_name_in -concrete_let_name -> compute_displayed_let_name_in -rename_rename_bound_var -> rename_bound_vars_as_displayed -lookup_name_as_renamed -> lookup_name_as_displayed -next_global_ident_away true -> next_ident_away_in_goal -next_global_ident_away false -> next_global_ident_away - -** Cleaning in commmand.ml - -Functions about starting/ending a lemma are in lemmas.ml -Functions about inductive schemes are in indschemes.ml - -Functions renamed: - -declare_one_assumption -> declare_assumption -declare_assumption -> declare_assumptions -Command.syntax_definition -> Metasyntax.add_syntactic_definition -declare_interning_data merged with add_notation_interpretation -compute_interning_datas -> compute_full_internalization_env -implicits_env -> internalization_env -full_implicits_env -> full_internalization_env -build_mutual -> do_mutual_inductive -build_recursive -> do_fixpoint -build_corecursive -> do_cofixpoint -build_induction_scheme -> build_mutual_induction_scheme -build_indrec -> build_induction_scheme -instantiate_type_indrec_scheme -> weaken_sort_scheme -instantiate_indrec_scheme -> modify_sort_scheme -make_case_dep, make_case_nodep -> build_case_analysis_scheme -make_case_gen -> build_case_analysis_scheme_default - -Types: - -decl_notation -> decl_notation option - -** Cleaning in libnames/nametab interfaces - -Functions: - -dirpath_prefix -> pop_dirpath -extract_dirpath_prefix pop_dirpath_n -extend_dirpath -> add_dirpath_suffix -qualid_of_sp -> qualid_of_path -pr_sp -> pr_path -make_short_qualid -> qualid_of_ident -sp_of_syntactic_definition -> path_of_syntactic_definition -sp_of_global -> path_of_global -id_of_global -> basename_of_global -absolute_reference -> global_of_path -locate_syntactic_definition -> locate_syndef -path_of_syntactic_definition -> path_of_syndef -push_syntactic_definition -> push_syndef - -Types: - -section_path -> full_path - -** Cleaning in parsing extensions (commit 12108) - -Many moves and renamings, one new file (Extrawit, that contains wit_tactic). - -** Cleaning in tactical.mli - -tclLAST_HYP -> onLastHyp -tclLAST_DECL -> onLastDecl -tclLAST_NHYPS -> onNLastHypsId -tclNTH_DECL -> onNthDecl -tclNTH_HYP -> onNthHyp -onLastHyp -> onLastHypId -onNLastHyps -> onNLastDecls -onClauses -> onClause -allClauses -> allHypsAndConcl - -+ removal of various unused combinators on type "clause" - -========================================= -= CHANGES BETWEEN COQ V8.1 AND COQ V8.2 = -========================================= - -A few differences in Coq ML interfaces between Coq V8.1 and V8.2 -================================================================ - -** Datatypes - -List of occurrences moved from "int list" to "Termops.occurrences" (an - alias to "bool * int list") -ETIdent renamed to ETName - -** Functions - -Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply -Tactics: apply_with_bindings -> apply_with_bindings_wo_evars -Eauto.simplest_apply -> Hiddentac.h_simplest_apply -Evarutil.define_evar_as_arrow -> define_evar_as_product -Old version of Tactics.assert_tac disappears -Tactics.true_cut renamed into Tactics.assert_tac -Constrintern.interp_constrpattern -> intern_constr_pattern -Hipattern.match_with_conjunction is a bit more restrictive -Hipattern.match_with_disjunction is a bit more restrictive - -** Universe names (univ.mli) - - base_univ -> type0_univ (* alias of Set is the Type hierarchy *) - prop_univ -> type1_univ (* the type of Set in the Type hierarchy *) - neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *) - is_base_univ -> is_type1_univ - is_empty_univ -> is_lower_univ - -** Sort names (term.mli) - - mk_Set -> set_sort - mk_Prop -> prop_sort - type_0 -> type1_sort - -========================================= -= CHANGES BETWEEN COQ V8.0 AND COQ V8.1 = -========================================= - -A few differences in Coq ML interfaces between Coq V8.0 and V8.1 -================================================================ - -** Functions - -Util: option_app -> option_map -Term: substl_decl -> subst_named_decl -Lib: library_part -> remove_section_part -Printer: prterm -> pr_lconstr -Printer: prterm_env -> pr_lconstr_env -Ppconstr: pr_sort -> pr_rawsort -Evd: in_dom, etc got standard ocaml names (i.e. mem, etc) -Pretyping: - - understand_gen_tcc and understand_gen_ltac merged into understand_ltac - - type_constraints can now say typed by a sort (use OfType to get the - previous behavior) -Library: import_library -> import_module - -** Constructors - -Declarations: mind_consnrealargs -> mind_consnrealdecls -NoRedun -> NoDup -Cast and RCast have an extra argument: you can recover the previous - behavior by setting the extra argument to "CastConv DEFAULTcast" and - "DEFAULTcast" respectively -Names: "kernel_name" is now "constant" when argument of Term.Const -Tacexpr: TacTrueCut and TacForward(false,_,_) merged into new TacAssert -Tacexpr: TacForward(true,_,_) branched to TacLetTac - -** Modules - -module Decl_kinds: new interface -module Bigint: new interface -module Tacred spawned module Redexpr -module Symbols -> Notation -module Coqast, Ast, Esyntax, Termast, and all other modules related to old - syntax are removed -module Instantiate: integrated to Evd -module Pretyping now a functor: use Pretyping.Default instead - -** Internal names - -OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE - -** Tactic extensions - -- printers have an extra parameter which is a constr printer at high precedence -- the tactic printers have an extra arg which is the expected precedence -- level is now a precedence in declare_extra_tactic_pprule -- "interp" functions now of types the actual arg type, not its encapsulation - as a generic_argument - -========================================= -= CHANGES BETWEEN COQ V7.4 AND COQ V8.0 = -========================================= - -See files in dev/syntax-v8 - - -============================================== -= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 = -============================================== - -CHANGES DUE TO INTRODUCTION OF MODULES -====================================== - -1.Kernel --------- - - The module level has no effect on constr except for the structure of -section_path. The type of unique names for constructions (what -section_path served) is now called a kernel name and is defined by - -type uniq_ident = int * string * dir_path (* int may be enough *) -type module_path = - | MPfile of dir_path (* reference to physical module, e.g. file *) - | MPbound of uniq_ident (* reference to a module parameter in a functor *) - | MPself of uniq_ident (* reference to one of the containing module *) - | MPdot of module_path * label -type label = identifier -type kernel_name = module_path * dir_path * label - ^^^^^^^^^^^ ^^^^^^^^ ^^^^^ - | | \ - | | the base name - | \ - / the (true) section path - example: (non empty only inside open sections) - L = (* i.e. some file of logical name L *) - struct - module A = struct Def a = ... end - end - M = (* i.e. some file of logical name M *) - struct - Def t = ... - N = functor (X : sig module T = struct Def b = ... end end) -> struct - module O = struct - Def u = ... - end - Def x := ... <M>.t ... <N>.O.u ... X.T.b ... L.A.a - - <M> and <N> are self-references, X is a bound reference and L is a -reference to a physical module. - - Notice that functor application is not part of a path: it must be -named by a "module M = F(A)" declaration to be used in a kernel -name. - - Notice that Jacek chose a practical approach, making directories not -modules. Another approach could have been to replace the constructor -MPfile by a constant constructor MProot representing the root of the -world. - - Other relevant informations are in kernel/entries.ml (type -module_expr) and kernel/declarations.ml (type module_body and -module_type_body). - -2. Library ----------- - -i) tables -[Summaries] - the only change is the special treatment of the -global environmet. - -ii) objects -[Libobject] declares persistent objects, given with methods: - - * cache_function specifying how to add the object in the current - scope; - * load_function, specifying what to do when the module - containing the object is loaded; - * open_function, specifying what to do when the module - containing the object is opened (imported); - * classify_function, specyfying what to do with the object, - when the current module (containing the object) is ended. - * subst_function - * export_function, to signal end_section survival - -(Almost) Each of these methods is called with a parameter of type -object_name = section_path * kernel_name -where section_path is the full user name of the object (such as -Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal -version such as (MPself<Datatypes#1>,[],"Fst") (see above) - - -What happens at the end of an interactive module ? -================================================== -(or when a file is stored and reloaded from disk) - -All summaries (except Global environment) are reverted to the state -from before the beginning of the module, and: - -a) the objects (again, since last Declaremods.start_module or - Library.start_library) are classified using the classify_function. - To simplify consider only those who returned Substitute _ or Keep _. - -b) If the module is not a functor, the subst_function for each object of - the first group is called with the substitution - [MPself "<Datatypes#1>" |-> MPfile "Coq.Init.Datatypes"]. - Then the load_function is called for substituted objects and the - "keep" object. - (If the module is a library the substitution is done at reloading). - -c) The objects which returned substitute are stored in the modtab - together with the self ident of the module, and functor argument - names if the module was a functor. - - They will be used (substituted and loaded) when a command like - Module M := F(N) or - Module Z := N - is evaluated - - -The difference between "substitute" and "keep" objects -======================================================== -i) The "keep" objects can _only_ reference other objects by section_paths -and qualids. They do not need the substitution function. - -They will work after end_module (or reloading a compiled library), -because these operations do not change section_path's - -They will obviously not work after Module Z:=N. - -These would typically be grammar rules, pretty printing rules etc. - - - -ii) The "substitute" objects can _only_ reference objects by -kernel_names. They must have a valid subst_function. - -They will work after end_module _and_ after Module Z:=N or -Module Z:=F(M). - - - -Other kinds of objects: -iii) "Dispose" - objects which do not survive end_module - As a consequence, objects which reference other objects sometimes - by kernel_names and sometimes by section_path must be of this kind... - -iv) "Anticipate" - objects which must be treated individually by - end_module (typically "REQUIRE" objects) - - - -Writing subst_thing functions -============================= -The subst_thing shoud not copy the thing if it hasn't actually -changed. There are some cool emacs macros in dev/objects.el -to help writing subst functions this way quickly and without errors. -Also there are *_smartmap functions in Util. - -The subst_thing functions are already written for many types, -including constr (Term.subst_mps), -global_reference (Libnames.subst_global), -rawconstr (Rawterm.subst_raw) etc - -They are all (apart from constr, for now) written in the non-copying -way. - - -Nametab -======= - -Nametab has been made more uniform. For every kind of thing there is -only one "push" function and one "locate" function. - - -Lib -=== - -library_segment is now a list of object_name * library_item, where -object_name = section_path * kernel_name (see above) - -New items have been added for open modules and module types - - -Declaremods -========== -Functions to declare interactive and noninteractive modules and module -types. - - -Library -======= -Uses Declaremods to actually communicate with Global and to register -objects. - - -OTHER CHANGES -============= - -Internal representation of tactics bindings has changed (see type -Rawterm.substitution). - -New parsing model for tactics and vernacular commands - - - Introduction of a dedicated type for tactic expressions - (Tacexpr.raw_tactic_expr) - - Introduction of a dedicated type for vernac expressions - (Vernacexpr.vernac_expr) - - Declaration of new vernacular parsing rules by a new camlp4 macro - GRAMMAR COMMAND EXTEND ... END to be used in ML files - - Declaration of new tactics parsing/printing rules by a new camlp4 macro - TACTIC EXTEND ... END to be used in ML files - -New organisation of THENS: -tclTHENS tac tacs : tacs is now an array -tclTHENSFIRSTn tac1 tacs tac2 : - apply tac1 then, apply the array tacs on the first n subgoals and - tac2 on the remaining subgoals (previously tclTHENST) -tclTHENSLASTn tac1 tac2 tacs : - apply tac1 then, apply tac2 on the first subgoals and apply the array - tacs on the last n subgoals -tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI) -tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs -tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|] -tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL) -tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number") -tclTHENSV same as tclTHENS but with an array -tclTHENSi : no longer available - -Proof_type: subproof field in type proof_tree glued with the ref field - -Tacmach: no more echo from functions of module Refiner - -Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v. -Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd - VERNAC COMMAND EXTEND macros -File syntax/PPTactic.v moved to parsing/pptactic.ml -Tactics about False and not now in tactics/contradiction.ml -Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v) -File tacinterp.ml moved from proofs to directory tactics - - -========================================== -= 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 |