========================================= = CHANGES BETWEEN COQ V8.7 AND COQ V8.8 = ========================================= * ML API * We removed the following functions: - Universes.unsafe_constr_of_global: use Global.constr_of_global_in_context instead. The returned term contains De Bruijn universe variables. If you don't depend on universes being instantiated, simply drop the context. - Universes.unsafe_type_of_global: same as above with Global.type_of_global_in_context We changed the type of the following functions: - Global.body_of_constant_body: now also returns the abstract universe context. The returned term contains De Bruijn universe variables. - Global.body_of_constant: same as above. ========================================= = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= * Ocaml * Coq is compiled with -safe-string enabled and requires plugins to do the same. This means that code using `String` in an imperative way will fail to compile now. They should switch to `Bytes.t` * Plugin API * Coq 8.7 offers a new module overlay containing a proposed plugin API in `API/API.ml`; this overlay is enabled by adding the `-open API` flag to the OCaml compiler; this happens automatically for developments in the `plugin` folder and `coq_makefile`. However, `coq_makefile` can be instructed not to enable this flag by passing `-bypass-API`. * ML API * Added two functions for declaring hooks to be executed in reduction functions when some given constants are traversed: declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv). set_reduction_effect: to declare a constant on which a given effect hook should be called. We renamed the following functions: Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr Printer.pr_var_list_decl -> Printer.pr_compacted_decl Printer.pr_var_decl -> Printer.pr_named_decl Nameops.lift_subscript -> Nameops.increment_subscript We removed the following functions: Termops.compact_named_context_reverse ... practical substitute is Termops.compact_named_context Namegen.to_avoid ... equivalent substitute is Names.Id.List.mem We renamed the following modules: Context.ListNamed -> Context.Compacted The following type aliases where removed Context.section_context ... it was just an alias for "Context.Named.t" which is still available The module Constrarg was merged into Stdarg. The following types have been moved and modified: local_binder -> local_binder_expr glob_binder merged with glob_decl The following constructors have been renamed: LocalRawDef -> CLocalDef LocalRawAssum -> CLocalAssum LocalPattern -> CLocalPattern In Constrexpr_ops: Deprecating abstract_constr_expr in favor of mkCLambdaN, and prod_constr_expr in favor of mkCProdN. Note: the first ones were interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type. In Nameops: The API has been made more uniform. New combinators added in the "Name" space name. Function "out_name" now fails with IsAnonymous rather than with Failure "Nameops.out_name". Location handling and AST attributes: Location handling has been reworked. First, Loc.ghost has been removed in favor of an option type, all objects carrying an optional source code location have been switched to use `Loc.t option`. Storage of location information has been also refactored. The main datatypes representing Coq AST (constrexpr, glob_expr) have been switched to a generic "node with attributes" representation `'a CAst.ast`, which is a record of the form: ```ocaml type 'a ast = private { v : 'a; loc : Loc.t option; ... } ``` consumers of AST nodes are recommended to use accessor-based pattern matching `{ v; loc }` to destruct `ast` object. Creation is done with `CAst.make ?loc obj`, where the attributes are optional. Some convenient combinators are provided in the module. A typical match: ``` | CCase(loc, a1) -> CCase(loc, f a1) ``` is now done as: ``` | { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1) ``` or even better, if plan to preserve the attributes you can wrap your top-level function in `CAst.map` to have: ``` | CCase(a1) -> CCase(f a1) ``` This scheme based on records enables easy extensibility of the AST node type without breaking compatibility. Not all objects carrying a location have been converted to the generic node representation, some of them may be converted in the future, for some others the abstraction is not just worth it. Thus, we still maintain a `'a Loc.located == Loc.t option * a'`, tuple type which should be treated as private datatype (ok to match against, but forbidden to manually build), and it is mandatory to use it for objects that carry a location. This policy has been implemented in the whole code base. Matching a located object hasn't changed, however, `Loc.tag ?loc obj` must be used to build one. In GOption: Support for non-synchronous options has been removed. Now all options are handled as a piece of normal document state, and thus passed to workers, etc... As a consequence, the field `Goptions.optsync` has been removed. In Coqlib / reference location: We have removed from Coqlib functions returning `constr` from names. Now it is only possible to obtain references, that must be processed wrt the particular needs of the client. We have changed in constrintern the functions returnin `constr` as well to return global references instead. Users of `coq_constant/gen_constant` can do `Universes.constr_of_global (find_reference dir r)` _however_ note the warnings in the `Universes.constr_of_global` in the documentation. It is very likely that you were previously suffering from problems with polymorphic universes due to using `Coqlib.coq_constant` that used to do this. You must rather use `pf_constr_of_global` in tactics and `Evarutil.new_global` variants when constructing terms in ML (see univpoly.txt for more information). ** Tactic API ** - pf_constr_of_global now returns a tactic instead of taking a continuation. Thus it only generates one instance of the global reference, and it is the caller's responsibility to perform a focus on the goal. - pf_global, construct_reference, global_reference, global_reference_in_absolute_module now return a global_reference instead of a constr. - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase was very specific. Use tclPROGRESS instead. - The unsafe flag of the Refine.refine function and its variants has been renamed and dualized into typecheck and has been made mandatory. ** Ltac API ** Many Ltac specific API has been moved in its own ltac/ folder. Amongst other important things: - Pcoq.Tactic -> Pltac - Constrarg.wit_tactic -> Tacarg.wit_tactic - Constrarg.wit_ltac -> Tacarg.wit_ltac - API below ltac/ that accepted a *_tactic_expr now accept a *_generic_argument instead - Some printing functions were moved from Pptactic to Pputils - A part of Tacexpr has been moved to Tactypes - The TacFun tactic expression constructor now takes a `Name.t list` for the variable list rather than an `Id.t option list`. The folder itself has been turned into a plugin. This does not change much, but because it is a packed plugin, it may wreak havoc for third-party plugins depending on any module defined in the ltac/ directory. Namely, even if everything looks OK at compile time, a plugin can fail to load at link time because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with an error of the form: Error: while loading myplugin.cmxs, no implementation available for Foo. In particular, most EXTEND macros will trigger this problem even if they seemingly do not use any Ltac module, as their expansion do. The solution is simple, and consists in adding a statement "open Ltac_plugin" in each file using a Ltac module, before such a module is actually called. An alternative solution would be to fully qualify Ltac modules, e.g. turning any call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not work for EXTEND macros though. ** Additional changes in tactic extensions ** Entry "constr_with_bindings" has been renamed into "open_constr_with_bindings". New entry "constr_with_bindings" now uses type classes and rejects terms with unresolved holes. ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For functions that used to carry a suffix `_loc`, such suffix has been dropped. - `errorlabstrm` and `error` has been removed in favor of `user_err`. - The header parameter to `user_err` has been made optional. ** Pretty printing ** Some functions have been removed, see pretty printing below for more details. * Pretty Printing and XML protocol * The type std_cmdpps has been reworked and made the canonical "Coq rich document type". This allows for a more uniform handling of printing (specially in IDEs). The main consequences are: - Richpp has been confined to IDE use. Most of previous uses of the `richpp` type should be replaced now by `Pp.std_cmdpps`. Main API has been updated. - The XML protocol will send a new message type of `pp`, which should be rendered client-wise. - `Set Printing Width` is deprecated, now width is controlled client-side. - `Pp_control` has removed. The new module `Topfmt` implements console control for the toplevel. - The impure tag system in Pp has been removed. This also does away with the printer signatures and functors. Now printers tag unconditionally. - The following functions have been removed from `Pp`: val stras : int * string -> std_ppcmds val tbrk : int * int -> std_ppcmds val tab : unit -> std_ppcmds val pifb : unit -> std_ppcmds val comment : int -> std_ppcmds val comments : ((int * int) * string) list ref val eval_ppcmds : std_ppcmds -> std_ppcmds val is_empty : std_ppcmds -> bool val t : std_ppcmds -> std_ppcmds val hb : int -> std_ppcmds val vb : int -> std_ppcmds val hvb : int -> std_ppcmds val hovb : int -> std_ppcmds val tb : unit -> std_ppcmds val close : unit -> std_ppcmds val tclose : unit -> std_ppcmds val open_tag : Tag.t -> std_ppcmds val close_tag : unit -> std_ppcmds val msg_with : ... module Tag ** Stm API ** - We have streamlined the `Stm` API, now `add` and `query` take a `coq_parsable` instead a `string` so clients can have more control over their input stream. As a consequence, their types have been modified. - The main parsing entry point has also been moved to the `Stm`. Parsing is considered a synchronous operation so it will either succeed or raise an exception. - `Feedback` is now only emitted for asynchronous operations. As a consequence, it always carries a valid stateid and the type has changed to accommodate that. - A few unused hooks were removed due to cleanups, no clients known. ** Toplevel and Vernacular API ** - The components related to vernacular interpretation have been moved to their own folder `vernac/` whereas toplevel now contains the proper toplevel shell and compiler. - Coq's toplevel has been ported to directly use the common `Stm` API. The signature of a few functions has changed as a result. ** XML Protocol ** - The legacy `Interp` call has been turned into a noop. - The `query` call has been modified, now it carries a mandatory "route_id" integer parameter, that associated the result of such query with its generated feedback. ========================================= = 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 := ... .t ... .O.u ... X.T.b ... L.A.a and 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,[],"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 "" |-> 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