path: root/dev/doc/changes.txt

=========================================
= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
=========================================

** 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}

** 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.

- 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 }
  
- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c`

=========================================
= 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