Updated.

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

2 files changed, 123 insertions, 16 deletions

diff --git a/contrib/xml/COPYRIGHT b/contrib/xml/COPYRIGHT
index a195efd5f2..c8d231fd3c 100644
--- a/contrib/xml/COPYRIGHT
+++ b/contrib/xml/COPYRIGHT
@@ -1,13 +1,25 @@
+(******************************************************************************)
+(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>     *)
+(*                          Project Helm   (http://helm.cs.unibo.it)          *)
+(*                          Project MoWGLI (http://mowgli.cs.unibo.it)        *)
+(*                                                                            *)
+(*                     Coq Exportation to XML                                 *)
+(*                                                                            *)
+(******************************************************************************)
+
 This Coq module has been developed by Claudio Sacerdoti Coen
-<sacerdot@cs.unibo.it> as a member of project HELM, to provide XML files
-to be used in the project.
+<sacerdot@cs.unibo.it> as a developer of projects HELM and MoWGLI.
+
 Project HELM (for Hypertextual Electronic Library of Mathematics) is a
 project developed at the Department of Computer Science, University of Bologna;
-http://www.cs.unibo.it/helm
+http://helm.cs.unibo.it
+
+Project MoWGLI (Mathematics on the Web: Get It by Logics and Interfaces)
+is a UE IST project that generalizes and extends the HELM project;
+http://mowgli.cs.unibo.it
 
-The author is interested in any other possible usage of the module.
-So, if you plan to use the module in other projects/development, please
-send him an e-mail.
+The author is interested in any possible usage of the module.
+So, if you plan to use the module, please send him an e-mail.
 
 The licensing policy applied to the module is the same as for the whole Coq
 distribution.
diff --git a/contrib/xml/README b/contrib/xml/README
index 46c8b42c5b..a45dd31a50 100644
--- a/contrib/xml/README
+++ b/contrib/xml/README
@@ -19,7 +19,7 @@ This document is tructured in the following way:
  2. Technical informations
    2.1. Inner-types
    2.2. CIC with Explicit Named Substitutions
-   2.3. The CIC XML DTD
+   2.3. The CIC with Explicit Named Substitutions XML DTD
 
 ================================================================================
                             USER DOCUMENTATION
@@ -148,12 +148,107 @@ exported appling the 3rd condition.
 The exported files are and XML encoding of the lambda-terms used by the
 Coq system. The implementative details of the Coq system are hidden as much
 as possible, so that the XML DTD is a straightforward encoding of the  
-Calculus of ...
-
-#TO BE FINISHED
-
-====================
-2.3. The CIC XML DTD
-====================
-
-#TO BE FINISHED
+Calculus of (Co)Inductive Constructions.
+
+Nevertheless, there is a feature of the Coq system that can not be
+hidden in a completely satisfactory way: discharging. In Coq it is possible
+to open a section, declare variables and use them in the rest of the section
+as if they were axiom declarations. Once the section is closed, every definition
+and theorem in the section is discharged by abstracting it over the section
+variables. Variable declarations as well as section declarations are entirely
+dropped. Since we are interested in an XML encoding of definitions and
+theorems as close as possible to those directly provided the user, we
+do not want to export discharged forms. Exporting non-discharged theorem
+and definitions together with theorems that rely on the discharged forms
+obliges the tools that work on the XML encoding to implement discharging to
+achieve logical consistency. Moreover, the rendering of the files can be
+misleading, since hyperlinks can be shown between occurrences of the discharge
+form of a definition and the non-discharged definition, that are different
+objects.
+
+To overcome the previous limitations, Claudio Sacerdoti Coen developed in his
+PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions
+with Explicit Named Substitutions, that is a slight extension of CIC where
+discharging is not necessary. The DTD of the exported XML files describes
+constants, inductive types and variables of the Calculus of (Co)Inductive
+Constructions with Explicit Named Substitions. The conversion to the new
+calculus is performed during the exportation phase.
+
+The following example shows a very small Coq development together with its
+version in CIC with Explicit Named Substitutions.
+
+# CIC version: #
+Section S.
+ Variable A : Prop.
+
+ Definition impl := A -> A.
+
+ Theorem t : impl.           (* uses the undischarged form of impl *)
+  Proof.
+   exact (fun (a:A) => a).
+  Qed.
+
+End S.
+
+Theorem t' : (impl False).   (* uses the discharged form of impl *) 
+ Proof.
+  exact (t False).           (* uses the discharged form of t *)
+ Qed.
+
+# Corresponding CIC with Explicit Named Substitutions version: #
+Section S.
+ Variable A : Prop.
+
+ Definition impl(A) := A -> A.   (* theorems and definitions are
+                                    explicitly abstracted over the
+                                    variables. The name is sufficient
+                                    to completely describe the abstraction *)
+
+ Theorem t(A) : impl.            (* impl where A is not instantiated *)
+  Proof.
+   exact (fun (a:A) => a).
+  Qed.
+
+End S.
+
+Theorem t'() : impl{False/A}.    (* impl where A is instantiated with False
+                                    Notice that t' does not depend on A     *) 
+ Proof.
+  exact t{False/A}.              (* t where A is instantiated with False *)
+ Qed.
+
+Further details on the typing and reduction rules of the calculus can be
+found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency
+of the calculus is also proved.
+
+======================================================
+2.3. The CIC with Explicit Named Substitutions XML DTD
+======================================================
+
+A copy of the DTD can be found in the file "cic.dtd".
+
+<ConstantType>     is the root element of the files that correspond to
+                   constant types.
+<ConstantBody>     is the root element of the files that correspond to
+                   constant bodies. It is used only for closed definitions and
+                   theorems (i.e. when no metavariable occurs in the body
+                   or type of the constant)
+<CurrentProof>     is the root element of the file that correspond to
+                   the body of a constant that depends on metavariables
+                   (e.g. unfinished proofs)
+<Variable>         is the root element of the files that correspond to variables
+<InductiveTypes>   is the root element of the files that correspond to blocks
+                   of mutually defined inductive definitions
+
+The elements
+ <LAMBDA>,<CAST>,<PROD>,<REL>,<SORT>,<APPLY>,<VAR>,<META>, <IMPLICIT>,<CONST>,
+ <LETIN>,<MUTIND>,<MUTCONSTRUCT>,<MUTCASE>,<FIX> and <COFIX>
+are used to encode the constructors of CIC. The sort or type attribute of the
+element, if present, is respectively the sort or the type of the term, that
+is a sort because of the typing rules of CIC.
+
+The element <instantiate> correspond to the application of an explicit named
+substitution to its first argument, that is a reference to a definition
+or declaration in the environment.
+
+All the other elements are just syntactic sugar.