Merge PR #962: Move dev/doc/changes to Markdown.

1 files changed, 348 insertions, 527 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.md
index 0f1a28028..5ed74917a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.md
@@ -1,141 +1,146 @@
-=========================================
-= CHANGES BETWEEN COQ V8.7 AND COQ V8.8 =
-=========================================
+## Changes between Coq 8.7 and Coq 8.8
 
-* ML API *
+### Plugin API
+
+Coq 8.8 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
 
 We removed the following functions:
 
-- Universes.unsafe_constr_of_global: use Global.constr_of_global_in_context
+- `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
+
+- `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.
+- `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.
+
+- `Global.body_of_constant`: same as above.
 
 We renamed the following datatypes:
 
-  Pp.std_ppcmds -> Pp.t
+- `Pp.std_ppcmds` -> `Pp.t`
 
-=========================================
-= CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
-=========================================
+## Changes between Coq 8.6 and Coq 8.7
 
-* Ocaml *
+### Ocaml
 
-Coq is compiled with -safe-string enabled and requires plugins to do
+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 *
+### ML 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
+- 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
+  * `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
+  * `set_reduction_effect`: to declare a constant on which a given effect
   hook should be called.
 
-We renamed the following functions:
+- 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:
+- 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
+  * `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:
+- We renamed the following modules:
 
-  Context.ListNamed -> Context.Compacted
+  * `Context.ListNamed` -> `Context.Compacted`
 
-The following type aliases where removed
+- The following type aliases where removed
 
-  Context.section_context    ... it was just an alias for "Context.Named.t" which is still available
+  * `Context.section_context`: it was just an alias for `Context.Named.t` which is still available.
 
-The module Constrarg was merged into Stdarg.
+- The module `Constrarg` was merged into `Stdarg`.
 
-The following types have been moved and modified:
+- The following types have been moved and modified:
 
-  local_binder -> local_binder_expr
-  glob_binder merged with glob_decl
+  * `local_binder` -> `local_binder_expr`
+  * `glob_binder` merged with `glob_decl`
 
-The following constructors have been renamed:
+- The following constructors have been renamed:
 
+  ```
   LocalRawDef -> CLocalDef
   LocalRawAssum -> CLocalAssum
   LocalPattern -> CLocalPattern
+  ```
 
-In Constrexpr_ops:
+- 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
+  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:
+- 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".
+  `Name` space name. Function `out_name` now fails with `IsAnonymous`
+  rather than with `Failure "Nameops.out_name"`.
 
-Location handling and AST attributes:
+- Location handling and AST attributes:
 
-  Location handling has been reworked. First, Loc.ghost has been
+  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
+  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;
-  ...
-}
-```
+  ```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)
-```
+
+  ```ocaml
+  | CCase(loc, a1) -> CCase(loc, f a1)
+  ```
+
   is now done as:
-```
-| { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1)
-```
+  ```ocaml
+  | { 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)
-```
+  ```ocaml
+  | CCase(a1) -> CCase(f a1)
+  ```
 
   This scheme based on records enables easy extensibility of the AST
   node type without breaking compatibility.
@@ -151,14 +156,14 @@ type 'a ast = private {
   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:
+- 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:
+- 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
@@ -175,65 +180,67 @@ In Coqlib / reference location:
   `pf_constr_of_global` in tactics and `Evarutil.new_global` variants
   when constructing terms in ML (see univpoly.txt for more information).
 
-** Tactic API **
+### Tactic API
 
-- pf_constr_of_global now returns a tactic instead of taking a continuation.
+- `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.
+- `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 `tclWEAK_PROGRESS` and `tclNOTSAMEGOAL` tacticals were removed. Their usecase
+  was very specific. Use `tclPROGRESS` instead.
 
 - New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows
   to iterate a non-unit tactic on all goals and access their returned values.
 
-- The unsafe flag of the Refine.refine function and its variants has been
+- 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 **
+### 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
+- `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 
+- 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
+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
+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
+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"
+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.
+call to Tacinterp into `Ltac_plugin.Tacinterp`. Note that this solution does not
+work for `EXTEND` macros though.
 
-** Additional changes in tactic extensions **
+### Additional changes in tactic extensions
 
-Entry "constr_with_bindings" has been renamed into
-"open_constr_with_bindings". New entry "constr_with_bindings" now
+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 **
+### 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
@@ -243,14 +250,14 @@ uses type classes and rejects terms with unresolved holes.
 
 - The header parameter to `user_err` has been made optional.
 
-** Pretty printing **
+### Pretty printing
 
 Some functions have been removed, see pretty printing below for more
 details.
 
-* Pretty Printing and XML protocol *
+#### Pretty Printing and XML protocol
 
-The type std_cmdpps has been reworked and made the canonical "Coq rich
+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:
 
@@ -267,12 +274,13 @@ document type". This allows for a more uniform handling of printing
  - `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
+ - 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`:
 
+   ```ocaml
    val stras : int * string -> std_ppcmds
    val tbrk  : int * int -> std_ppcmds
    val tab   : unit -> std_ppcmds
@@ -294,8 +302,9 @@ document type". This allows for a more uniform handling of printing
    val msg_with  : ...
 
    module Tag
+   ```
 
-** Stm API **
+### 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
@@ -312,7 +321,7 @@ document type". This allows for a more uniform handling of printing
 
 - A few unused hooks were removed due to cleanups, no clients known.
 
-** Toplevel and Vernacular API **
+### Toplevel and Vernacular API
 
 - The components related to vernacular interpretation have been moved
   to their own folder `vernac/` whereas toplevel now contains the
@@ -321,39 +330,41 @@ document type". This allows for a more uniform handling of printing
 - 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 **
+### 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
+  `route_id` integer parameter, that associated the result of such
   query with its generated feedback.
 
-=========================================
-= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
-=========================================
+## Changes between Coq 8.5 and Coq 8.6
 
-** Parsing **
+### Parsing
 
-Pcoq.parsable now takes an extra optional filename argument so as to
+`Pcoq.parsable` now takes an extra optional filename argument so as to
 bind locations to a file name when relevant.
 
-** Files **
+### 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/
+All IDE-specific files, including the XML protocol have been moved to `ide/`
 
-** Reduction functions **
+### Reduction functions
 
-In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX,
-fCOFIX.
+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
@@ -380,9 +391,11 @@ 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
@@ -392,15 +405,16 @@ 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.
+In `intf/genredexpr.mli`, `fIota` was replaced by `FMatch`, `FFix` and
+`FCofix`. Similarly, `rIota` was replaced by `rMatch`, `rFix` and `rCofix`.
 
-** Notation_ops **
+### Notation_ops
 
-Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr.
+Use `Glob_ops.glob_constr_eq` instead of `Notation_ops.eq_glob_constr`.
 
-** Logging and Pretty Printing: **
+### Logging and Pretty Printing
 
 * Printing functions have been removed from `Pp.mli`, which is now a
   purely pretty-printing interface. Functions affected are:
@@ -429,7 +443,7 @@ val message     : string -> unit
 
 * 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:
+  level. Functions moved from `Pp` to `Feedback` are:
 
 ```` ocaml
 val set_logger      : logger -> unit
@@ -474,12 +488,13 @@ val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
 val get_id_for_feedback : unit -> edit_or_state_id * route_id
 ````
 
-** Kernel API changes **
+### Kernel API changes
 
-- The interface of the Context module was changed.
+- 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
@@ -521,123 +536,142 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id
     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
+    ```ocaml
+    type 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
- 
+    ```ocaml
+    type 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
+    ```ocaml
+    type 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
+    ```ocaml
+    type 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
+- 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
+  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
+  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.
+  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.
+- `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.
+- The `Refine` module was moved out of `Proofview`.
 
+    ```
     Proofview.Refine.* --->  Refine.*
+    ```
 
-- A statically monotonous evarmap type was introduced in Sigma. Not all the API
+- A statically monotonic 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
+  `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:
 
+  ```ocaml
   let (sigma, x1) = ... in
   ...
   let (sigma, xn) = ... in
   (sigma, ans)
+  ```
 
   should be turned into:
 
+  ```ocaml
   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
+- The `Proofview.Goal.`*`enter` family of functions now takes a polymorphic
   continuation given as a record as an argument.
 
+  ```ocaml
   Proofview.Goal.enter begin fun gl -> ... end
+  ```
 
   should be turned into
 
+  ```ocaml
   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`)
+- `Global.named_context`                                         ---> `Global.named_context_val`
+- `Context.Named.lookup`                                         ---> `Environ.lookup_named_val`
 
-** Search API **
+### 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 =
-=========================================
+## Changes between Coq 8.4 and Coq 8.5
 
-** Refactoring : more mli interfaces and simpler grammar.cma **
+### 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
+  * `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
+  * 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).
@@ -686,11 +720,11 @@ printing.
   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).
+  `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).
 
@@ -704,36 +738,34 @@ printing.
 - 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 =
-=========================================
+## Changes between Coq 8.3 and Coq 8.4
 
-** Functions in unification.ml have now the evar_map coming just after the env
+- Functions in unification.ml have now the evar_map coming just after the env
 
-** Removal of Tacinterp.constr_of_id **
+- Removal of Tacinterp.constr_of_id
 
 Use instead either global_reference or construct_reference in constrintern.ml.
 
-** Optimizing calls to Evd functions **
+- 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 **
+- 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 **
+- ARGUMENT EXTEND
 
 It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED
 in ARGUMENT EXTEND statements.
 
-** Renaming of rawconstr to glob_constr **
+- 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
@@ -743,62 +775,67 @@ scripts to migrate code using Coq's internals, see commits 13743,
 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 =
-=========================================
+## Changes between Coq 8.2 and Coq 8.3
 
-** Light cleaning in evarutil.ml **
+### Light cleaning in evaruil.ml
 
 whd_castappevar is now whd_head_evar
 obsolete whd_ise disappears
 
-** Restructuration of the syntax of binders **
+### 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 **
+### 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
+### 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)
+ - apply_with_ebindings (use instead apply_with_bindings)
+ - eapply_with_ebindings (use instead eapply_with_bindings)
 
-** Obsolete functions in typing.ml
+### Obsolete functions in typing.ml
 
 For mtype_of, msort_of, mcheck, now use type_of, sort_of, check
 
-** Renaming functions renamed
+### 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
+### 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
@@ -815,15 +852,17 @@ 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
+### Cleaning in libnames/nametab interfaces
 
 Functions:
 
+```
 dirpath_prefix -> pop_dirpath
 extract_dirpath_prefix pop_dirpath_n
 extend_dirpath -> add_dirpath_suffix
@@ -837,17 +876,19 @@ 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)
+### Cleaning in parsing extensions (commit 12108)
 
 Many moves and renamings, one new file (Extrawit, that contains wit_tactic).
 
-** Cleaning in tactical.mli
+### Cleaning in tactical.mli
 
+```
 tclLAST_HYP -> onLastHyp
 tclLAST_DECL -> onLastDecl
 tclLAST_NHYPS -> onNLastHypsId
@@ -857,24 +898,21 @@ 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 =
-=========================================
+and removal of various unused combinators on type "clause"
 
-A few differences in Coq ML interfaces between Coq V8.1 and V8.2
-================================================================
+## Changes between Coq 8.1 and Coq 8.2
 
-** Datatypes
+### Datatypes
 
 List of occurrences moved from "int list" to "Termops.occurrences" (an
   alias to "bool * int list")
 ETIdent renamed to ETName
 
-** Functions
+### 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
@@ -884,98 +922,93 @@ 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)
+### Universe names (univ.mli)
 
+ ```ocaml
  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)
+### 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
+  ```
+
+## Changes between Coq 8.0 and Coq 8.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
+ * 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
+### 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
+ * 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
+### Internal names
 
 OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE
 
-** Tactic extensions
+### 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
+ * 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 =
-=========================================
+## Changes between Coq 7.4 and Coq 8.0
 
 See files in dev/syntax-v8
 
 
-==============================================
-= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 =
-==============================================
+## Main changes between Coq 7.4 and Coq 8.0
 
-CHANGES DUE TO INTRODUCTION OF MODULES
-======================================
+### Changes due to introduction of modules
 
-1.Kernel
---------
+#### 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
  
+```ocaml
 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 *)
@@ -1002,7 +1035,8 @@ type kernel_name = module_path * dir_path * label
          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.
  
@@ -1019,14 +1053,13 @@ world.
 module_expr) and kernel/declarations.ml (type module_body and
 module_type_body).                                                              
 
-2. Library
-----------
+#### Library
 
-i) tables 
+1. tables
 [Summaries] - the only change is the special treatment of the
 global environmet.
 
-ii) objects 
+2. objects 
 [Libobject] declares persistent objects, given with methods:
 
    * cache_function specifying how to add the object in the current
@@ -1047,25 +1080,25 @@ 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 ?
-==================================================
+#### 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
+1. 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
+2. 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
+3. 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.
 
@@ -1075,9 +1108,9 @@ c) The objects which returned substitute are stored in the modtab
    is evaluated
 
 
-The difference between "substitute" and "keep" objects
-========================================================
-i) The "keep" objects can _only_ reference other objects by section_paths
+#### The difference between "substitute" and "keep" objects
+
+1. 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),
@@ -1089,7 +1122,7 @@ These would typically be grammar rules, pretty printing rules etc.
 
 
 
-ii) The "substitute" objects can _only_ reference objects by
+2. 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 
@@ -1098,17 +1131,18 @@ Module Z:=F(M).
 
 
 Other kinds of objects:
-iii) "Dispose" - objects which do not survive end_module
+
+3. "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
+4. "Anticipate" - objects which must be treated individually by
     end_module (typically "REQUIRE" objects)
 
 
 
-Writing subst_thing functions
-=============================
+#### 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.
@@ -1123,15 +1157,13 @@ They are all (apart from constr, for now) written in the non-copying
 way.
 
 
-Nametab
-=======
+#### Nametab
 
 Nametab has been made more uniform. For every kind of thing there is
 only one "push" function and one "locate" function. 
 
 
-Lib
-===
+#### Lib
 
 library_segment is now a list of object_name * library_item, where
 object_name = section_path * kernel_name (see above)
@@ -1139,20 +1171,19 @@ object_name = section_path * kernel_name (see above)
 New items have been added for open modules and module types
 
 
-Declaremods
-==========
+#### Declaremods
+
 Functions to declare interactive and noninteractive modules and module
 types.
 
 
-Library
-=======
+#### Library
+
 Uses Declaremods to actually communicate with Global and to register
 objects.
 
 
-OTHER CHANGES
-=============
+### Other changes
 
 Internal representation of tactics bindings has changed (see type
 Rawterm.substitution).
@@ -1169,258 +1200,48 @@ New parsing model for tactics and vernacular commands
     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 :
+
+- 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 :
+- 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
+- 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 =
-==========================================
+## Changes between Coq 7.1 and Coq 7.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
+- 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