Documentation of CHANGES and refman doc for the implicit argument binder

`X`.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10538 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 54 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index d45698d5bc..926b7002d6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,10 +7,11 @@ Language
   all arguments are tried successively (from left to right) until one is 
   found that satisfies the structural decreasing condition.
 - Improved inference of implicit arguments.
-- New experimental typeclass system giving ad-hoc polymorphism and overloading based on 
-  dependent records and implicit arguments.
-- New syntax "let| pat := b in c" for binding using irrefutable patterns.
-- New syntax "forall `A`, T" for specifying maximally inserted implicit arguments in terms.
+- New experimental typeclass system giving ad-hoc polymorphism and 
+  overloading based on dependent records and implicit arguments.
+- New syntax "let| pat := b in c" for let-binding using irrefutable patterns.
+- New syntax "forall `A`, T" for specifying maximally inserted implicit 
+  arguments in terms.
 
 Commands
 
@@ -127,24 +128,35 @@ Type Classes
 - New "Class", "Instance" and "Program Instance" commands to define
   classes and instances documented in the reference manual.  
 - New binding construct " [ Class_1 param_1 .. param_n, Class_2 ... ] " 
-  for binding type classes usable everywhere.  
+  for binding type classes, usable everywhere.  
 - New command " Print Classes " and " Print Instances some_class " to
   print tables for typeclasses.  
 - New default eauto hint database "typeclass_instances" used by the default
   typeclass instance search tactic.  
-- New command " Instanciation Tactic := tac " to customize the typeclass
-  instance search tactic.
-- New theories directory "theories/Classes"
-
+- New theories directory "theories/Classes" for standard typeclasses 
+  declarations. Module Classes.Relations is a typeclass port of 
+  Relation_Definitions.
+- New experimental "setoid" rewriting tactic "clrewrite" based on typeclasses.
+  Classes.Morphisms declares standard morphisms, Classes.SetoidClasses declares 
+  the new Setoid typeclass.  
+  
 Program
 
 - Moved useful tactics in theories/Program and documented them.
+- Add Program.Basics which contains standard definitions for functional 
+  programming (id, apply, flip...)
 - More robust obligation handling, dependent pattern-matching and
   well-founded definitions.
 - New syntax " dest term as pat in term " for destructing objects using
   an irrefutable pattern while keeping equalities (use this instead of 
   "let" in Programs).
-
+- Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer 
+  which argument decreases structurally.
+- Program Lemma, Axiom etc... now permit to have obligations in the statement iff 
+  they can be automatically solved by the default tactic.
+- New command "Preterm [ of id ]" to see the actual term fed to Coq for
+  debugging purposes.
+  
 Miscellaneous
 
 - Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 01a0e9cad1..3a834ff8a8 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1125,8 +1125,35 @@ possible, the correct argument will be automatically generated.
 
 In case one wants that some arguments of a given object (constant,
 inductive types, constructors, assumptions, local or not) are always
-inferred by Coq, one may declare once for all which are the expected
-implicit arguments of this object. The syntax is
+inferred by Coq, one may declare once and for all which are the expected
+implicit arguments of this object. There are two ways to do this,
+a-priori and a-posteriori. 
+
+\subsubsection{Implicit Argument Binders}
+
+In the first setting, one wants to explicitely give the implicit
+arguments of a constant as part of its definition. To do this, one has
+to surround the bindings of implicit arguments by backquotes:
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+\begin{coq_example}
+Definition id `A : Type` (x : A) : A := x.
+\end{coq_example}
+
+This automatically declares the argument {\tt A} of {\tt id} as a
+maximally inserted implicit argument. One can then do as-if the argument
+was absent in every situation but still be able to specify it if needed:
+\begin{coq_example}
+Definition compose `A B C` (g : B -> C) (f : A -> B) := 
+  fun x => g (f x).
+Goal forall A, compose id id = id (A:=A).
+\end{coq_example}
+
+\subsubsection{The Implicit Arguments Vernacular Command}
+
+To set implicit arguments for a constant a-posteriori, one can use the
+command:
 \begin{quote}
 \tt Implicit Arguments {\qualid} [ \nelist{\possiblybracketedident}{} ]
 \end{quote}
@@ -1162,9 +1189,11 @@ Implicit Arguments length [[A]]. (* A has to be maximally inserted *)
 Check (fun l:list (list nat) => map length l).
 \end{coq_example}
 
-\Rem To know which are the implicit arguments of an object, use command
+\Rem To know which are the implicit arguments of an object, use the command
 {\tt Print Implicit} (see \ref{PrintImplicit}).
 
+\Rem 
+
 \Rem If the list of arguments is empty, the command removes the
 implicit arguments of {\qualid}.