diff options
Diffstat (limited to 'dev/doc/changes.txt')
| -rw-r--r-- | dev/doc/changes.txt | 278 |
1 files changed, 277 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 2f62be9a..3de938d7 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,5 +1,281 @@ ========================================= -= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 = += 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 ** |