Merge branch 'trunk' into pr379

3 files changed, 229 insertions, 74 deletions

diff --git a/dev/doc/api.txt b/dev/doc/api.txt
new file mode 100644
index 0000000000..5827257b53
--- /dev/null
+++ b/dev/doc/api.txt
@@ -0,0 +1,10 @@
+Recommendations in using the API:
+
+The type of terms: constr (see kernel/constr.ml and kernel/term.ml)
+
+- On type constr, the canonical equality on CIC (up to
+  alpha-conversion and cast removal) is Constr.equal
+- The type constr is abstract, use mkRel, mkSort, etc. to build
+  elements in constr; use "kind_of_term" to analyze the head of a
+  constr; use destRel, destSort, etc. when the head constructor is
+  known
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index f54f3fcc8e..03742fb8ad 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,12 @@
 = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
 =========================================
 
+* Ocaml *
+
+Coq is compiled with -safe-string enabled and requires plugins to do
+the same. This means that code using `String` in an imperative way
+will fail to compile now. They should switch to `Bytes.t`
+
 * ML API *
 
 We renamed the following functions:
@@ -39,6 +45,26 @@ important things:
   instead
 - Some printing functions were moved from Pptactic to Pputils
 - A part of Tacexpr has been moved to Tactypes
+- The TacFun tactic expression constructor now takes a `Name.t list` for the 
+  variable list rather than an `Id.t option list`.
+
+The folder itself has been turned into a plugin. This does not change much,
+but because it is a packed plugin, it may wreak havoc for third-party plugins
+depending on any module defined in the ltac/ directory. Namely, even if
+everything looks OK at compile time, a plugin can fail to load at link time
+because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with
+an error of the form:
+
+Error: while loading myplugin.cmxs, no implementation available for Foo.
+
+In particular, most EXTEND macros will trigger this problem even if they
+seemingly do not use any Ltac module, as their expansion do.
+
+The solution is simple, and consists in adding a statement "open Ltac_plugin"
+in each file using a Ltac module, before such a module is actually called. An
+alternative solution would be to fully qualify Ltac modules, e.g. turning any
+call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not
+work for EXTEND macros though.
 
 ** Error handling **
 
@@ -50,6 +76,58 @@ important things:
 
 - The header parameter to `user_err` has been made optional.
 
+** Pretty printing **
+
+Some functions have been removed, see pretty printing below for more
+details.
+
+* Pretty Printing and XML protocol *
+
+The type std_cmdpps has been reworked and made the canonical "Coq rich
+document type". This allows for a more uniform handling of printing
+(specially in IDEs). The main consequences are:
+
+ - Richpp has been confined to IDE use. Most of previous uses of the
+   `richpp` type should be replaced now by `Pp.std_cmdpps`. Main API
+   has been updated.
+
+ - The XML protocol will send a new message type of `pp`, which should
+   be rendered client-wise.
+
+ - `Set Printing Width` is deprecated, now width is controlled
+   client-side.
+
+ - `Pp_control` has removed. The new module `Topfmt` implements
+   console control for the toplevel.
+
+ - The impure tag system in Pp has been removed. This also does away
+   with the printer signatures and functors. Now printers tag
+   unconditionally.
+
+ - The following functions have been removed from `Pp`:
+
+   val stras : int * string -> std_ppcmds
+   val tbrk  : int * int -> std_ppcmds
+   val tab   : unit -> std_ppcmds
+   val pifb  : unit -> std_ppcmds
+   val comment  : int -> std_ppcmds
+   val comments : ((int * int) * string) list ref
+   val eval_ppcmds : std_ppcmds -> std_ppcmds
+   val is_empty : std_ppcmds -> bool
+   val t : std_ppcmds -> std_ppcmds
+   val hb : int -> std_ppcmds
+   val vb : int -> std_ppcmds
+   val hvb : int -> std_ppcmds
+   val hovb : int -> std_ppcmds
+   val tb : unit -> std_ppcmds
+   val close : unit -> std_ppcmds
+   val tclose : unit -> std_ppcmds
+   val open_tag : Tag.t -> std_ppcmds
+   val close_tag : unit -> std_ppcmds
+   val msg_with  : ...
+
+   module Tag
+
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
diff --git a/dev/doc/style.txt b/dev/doc/style.txt
index 27695a09b1..2ee3dadd77 100644
--- a/dev/doc/style.txt
+++ b/dev/doc/style.txt
@@ -1,75 +1,142 @@
-
-<< L'uniformité du style est plus importante que le style lui-même. >>
-(Kernigan & Pike, The Practice of Programming)
-
-Mode Emacs
-==========
-   Tuareg, que l'on trouve ici :  http://www.prism.uvsq.fr/~acohen/tuareg/
-
-   avec le réglage suivant :     (setq tuareg-in-indent 2)
-
-Types récursifs et filtrages
-============================
-   Une barre de séparation y compris sur le premier constructeur
-
-type t =
-  | A 
-  | B of machin
-
-match expr with
-  | A -> ...
-  | B x -> ...
-
-Remarque : à partir de la 8.2 environ, la tendance est à utiliser le
-format suivant qui permet de limiter l'escalade d'indentation tout en
-produisant un aspect visuel intéressant de bloc :
-
-type t =
-| A 
-| B of machin
-
-match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = match expr with
-| A -> ...
-| B x -> ...
-
-let f expr = function
-| A -> ...
-| B x -> ...
-
-Le deuxième cas est obtenu sous tuareg avec les réglages
-
-  (setq tuareg-with-indent 0)
-  (setq tuareg-function-indent 0)
-  (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien 
-                                      /// pour les let mais pas pour les let-in
-
-Conditionnelles
-===============
-  if condition then
-    premier-cas
-  else
-    deuxieme-cas
-
-  Si effets de bord dans les branches, utilisez begin ... end et non des
-  parenthèses i.e.
-
-  if condition then begin
-    instr1;
-    instr2
-  end else begin
-    instr3;
-    instr4
-  end
-    
-  Si la première branche lève une exception, évitez le else i.e.
-
-    if condition then                     if condition then error "machin";
-      error "machin"          ----->      suite
+<< Style uniformity is more important than style itself >>
+   (Kernigan & Pike, The Practice of Programming)
+
+OCaml Style:
+- Spacing and indentation
+  - indent your code (using tuareg default)
+  - no strong constraints in formatting "let in"; possible styles are:
+    "let x = ... in"
+    "let x =
+       ... in"
+    "let
+       x = ...
+     in"
+  - but: no extra indentation before a "in" coming on next line,
+    otherwise, it first shifts further and further on the right,
+    reducing the amount of space available; second, it is not robust to
+    insertion of a new "let"
+  - it is established usage to have space around "|" as in
+    "match c with
+     | [] | [a] -> ...
+     | a::b::l -> ..."
+  - in a one-line "match", it is preferred to have no "|" in front of
+    the first case (this saves spaces for the match to hold in the line)
+  - from about 8.2, the tendency is to use the following format which
+    limit excessive indentation while providing an interesting "block" aspect
+    type t =
+    | A 
+    | B of machin
+
+    let f expr = match expr with
+    | A -> ...
+    | B x -> ...
+
+    let f expr = function
+    | A -> ...
+    | B x -> ...
+  - add spaces around = and == (make the code "breaths")
+  - the common usage is to write "let x,y = ... in ..." rather than
+    "let (x,y) = ... in ..."
+  - parenthesizing with either "(" and ")" or with "begin" and "end" is
+    common practice
+  - preferred layout for conditionals:
+    if condition then
+      premier-cas
     else
-      suite
-
-  
+      deuxieme-cas
+  - in case of effects in branches, use "begin ... end" rather than
+    parentheses
+    if condition then begin
+      instr1;
+      instr2
+    end else begin
+      instr3;
+      instr4
+    end
+  - if the first branch raises an exception, avoid the "else", i.e.:
+    if condition then                     if condition then error "foo";
+      error "foo"          ----->         bar
+    else
+      bar
+  - it is the usage not to use ;; to end OCaml sentences (however,
+    inserting ";;" can be useful for debugging syntax errors crossing
+    the boundary of functions)
+  - relevant options in tuareg:
+    (setq tuareg-in-indent 2)
+    (setq tuareg-with-indent 0)
+    (setq tuareg-function-indent 0)
+    (setq tuareg-let-always-indent nil)
+
+- Coding methodology
+  - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C),
+    Out_of_memory, Stack_overflow, etc.
+    at least, use "try with e when Errors.noncritical e -> ..."
+    (to be detailed, Pierre L. ?)
+  - do not abuse of fancy combinators: sometimes what a "let rec" loop
+    does is more readable and simpler to grasp than what a "fold" does
+  - do not break abstractions: if an internal property is hidden
+    behind an interface, do no rely on it in code which uses this
+    interface (e.g. do not use List.map thinking it is left-to-right,
+    use map_left)
+  - in particular, do not use "=" on abstract types: there is no
+    reason a priori that it is the intended equality on this type; use the
+    "equal" function normally provided with the abstract type
+  - avoid polymorphically typed "=" whose implementation is not
+    optimized in OCaml and which has moreover no reason to be the
+    intended implementation of the equality when it comes to be
+    instantiated on a particular type (e.g. use List.mem_f,
+    List.assoc_f, rather than List.mem, List.assoc, etc, unless it is
+    absolutely clear that "=" will implement the intended equality, and
+    with the right complexity)
+  - any new general-purpose enough combinator on list should be put in
+    cList.ml, on type option in cOpt.ml, etc.
+  - unless of a good reason not to so, follow the style of the
+    surrounding code in the same file as much as possible,
+    the general guidelines are otherwise "let spacing breaths" (we
+    have large screen nowadays), "make your code easy to read and
+    to understand"
+  - document what is tricky, but do not overdocument, sometimes the
+    choice of names and the structuration of the code is a better
+    documentation than a long discourse; use of unicode in comments is
+    welcome if it can make comments more readable (then
+    "toggle-enable-multibyte-characters" can help when using the
+    debugger in emacs)
+  - all of initial "open File", or of small-scope File.(...), or
+    per-ident File.foo are common practices
+
+- Choice of variable names
+  - be consistent when naming from one function to another
+  - be consistent with the naming adopted in the functions from the
+    same file, or with the naming used elsewhere by similar functions
+  - use variable names which express meaning
+  - keep "cst" for constants and avoid it for constructors which is
+    otherwise a source of confusion
+  - for constructors, use "cstr" in type constructor (resp. "cstru" in
+    constructor puniverse); avoid "constr" for "constructor" which
+    could be think as the name of an arbitrary Constr.t
+  - for inductive types, use "ind" in the type inductive (resp "indu"
+    in inductive puniverse)
+  - for env, use "env"
+  - for evar_map, use "sigma", with tolerance into "evm" and "evd"
+  - for named_context or rel_context, use "ctxt" or "ctx" (or "sign")
+  - for formal/actual indices of inductive types: "realdecls", "realargs"
+  - for formal/actual parameters of inductive types: "paramdecls", "paramargs"
+  - for terms, use e.g. c, b, a, ...
+  - if a term is known to be a function: f, ...
+  - if a term is known to be a type: t, u, typ, ...
+  - for a declaration, use d or "decl"
+  - for errors, exceptions, use e
+
+- Common OCaml pitfalls
+  - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in
+    "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in
+    parentheses are needed around the "try" and the inner "match"
+  - even if stream are lazy, the Pp.(++) combinator is strict and
+    forces the evaluation of its arguments (use a "lazy" or a "fun () ->")
+    to make it lazy explicitly
+  - in "if ... then ... else ... ++ ...", the default parenthesizing
+    is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..."
+  - in "let myspecialfun = mygenericfun args", be sure that it does no
+    do side-effect; prefer otherwise "let mygenericfun arg =
+    mygenericfun args arg" to ensure that the function is evaluated at
+    runtime