diff options
Diffstat (limited to 'dev/doc/changes.txt')
| -rw-r--r-- | dev/doc/changes.txt | 184 |
1 files changed, 183 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 2f62be9aff..4135ddd2db 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,5 +1,187 @@ ========================================= -= CHANGES BETWEEN COQ V8.4 AND CQQ V8.5 = += CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = +========================================= + +** 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. + +* 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 +```` + +* 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_info : Pp.std_ppcmds -> unit +val msg_notice : Pp.std_ppcmds -> unit +val msg_warning : Pp.std_ppcmds -> unit +val msg_error : Pp.std_ppcmds -> unit +val msg_debug : 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 +```` + +- 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.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.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. + +- 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) + +- 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 } + +========================================= += CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = ========================================= ** Refactoring : more mli interfaces and simpler grammar.cma ** |