- Documentation de admit et Print Assumptions.

- Relecture, mise à jour, correction d'erreurs et petite
  réorganisation du chapitre sur les commandes vernaculaires.
- Correction bug #1865 (rafraichissement des univers algébriques).
- Suppression de la dépendance du initial.coq en les noms longs des fichiers
  de façons à ce que les dépendances ne soient que purement logique.
- Encore un (petit) bug undo ide.	


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

10 files changed, 285 insertions, 262 deletions

diff --git a/CHANGES b/CHANGES
index 4271001293..5cf6e5ae6e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -48,6 +48,8 @@ Vernacular commands
   conversion tests. It generalizes commands Opaque and Transparent by
   introducing a range of levels. Lower levels are assigned to constants
   that should be expanded first.
+- New command "Print Assumptions" to display all variables, parameters
+  or axioms a theorem or definition relies on.
 
 Libraries (DOC TO CHECK)
 
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index caa75d977c..12cfacbc49 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -355,6 +355,9 @@ Check T. (* Now correct *)
 Reset Mod.
 \end{coq_eval}
 
+Some features defined in modules are activated only when a module is
+imported. This is for instance the case of notations (see
+Section~\ref{Notation}).
 
 \begin{Variants}
 \item{\tt Export {\qualid}}\comindex{Export}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 9a17c0f3c7..76faac5935 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -23,7 +23,8 @@ global constant.
 This displays various informations about the object denoted by {\qualid}:
 its kind (module, constant, assumption, inductive,
 constructor, abbreviation\ldots), long name, type, implicit
-arguments and argument scopes.
+arguments and argument scopes. It does not print the body of
+definitions or proofs.
 
 %\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
 %In case \qualid\ denotes an opaque theorem defined in a section,
@@ -83,87 +84,13 @@ displayed as in \Coq\ terms.
 
 \SeeAlso Chapter~\ref{Extraction}.
 
-\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command tells not to unfold
-the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
-$\delta$-conversion. Unfolding a constant is replacing it by its
-definition. {\tt Opaque} can only apply on constants originally
-defined as {\tt Transparent}.
+\subsection[\tt Print Assumptions {\qualid}.]{\tt Print Assumptions {\qualid}.\comindex{Print Assumptions}}
+\label{PrintAssumptions}
 
-Constants defined by a proof ended by {\tt Qed} are automatically
-stamped as {\tt Opaque} and can no longer be considered as {\tt
-Transparent}. This is to keep with the usual mathematical practice of
-{\em proof irrelevance}: what matters in a mathematical development is
-the sequence of lemma statements, not their actual proofs. This
-distinguishes lemmas from the usual defined constants, whose actual
-values are of course relevant in general.
-
-\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
-\ref{Theorem}
-
-\begin{ErrMsgs}
-\item \errindex{The reference \qualid\ was not found in the current
-environment}\\
-    There is no constant referred by {\qualid} in the environment.
-    Nevertheless, if you asked \texttt{Opaque foo bar}
-    and if \texttt{bar} does not exist, \texttt{foo} is set opaque.
-\end{ErrMsgs}
-
-\subsection[\tt Transparent \qualid$_1$ \dots \qualid$_n$.]{\tt Transparent \qualid$_1$ \dots \qualid$_n$.\comindex{Transparent}\label{Transparent}}
-This command is the converse of {\tt Opaque} and can only apply on constants originally defined as {\tt Transparent} to restore their initial behaviour after an {\tt Opaque} command.
-
-The constants automatically declared transparent are the ones defined by a proof ended by {\tt Defined}, or by a {\tt
-  Definition} or {\tt Local} with an explicit body.
-
-\Warning {\tt Transparent} and \texttt{Opaque} are not synchronous
-with the reset mechanism. If a constant was transparent at point A, if
-you set it opaque at point B and reset to point A, you return to state
-of point A with the difference that the constant is still opaque. This
-can cause changes in tactic scripts behaviour.
-
-At section or module closing, a constant recovers the status it got at
-the time of its definition.
-
-\begin{ErrMsgs}
-% \item \errindex{Can not set transparent.}\\
-%     It is a constant from a required module or a parameter.
-\item \errindex{The reference \qualid\ was not found in the current
-environment}\\
-    There is no constant referred by {\qualid} in the environment.
-\end{ErrMsgs}
-
-\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
-\ref{Theorem}
-
-
-\subsection{\tt Strategy {\it level} [ \qualid$_1$ \dots \qualid$_n$
-  ].\comindex{Strategy}\comindex{Local Strategy}\label{Strategy}}
-This command generalizes the behaviour of {\tt Opaque} and {\tt
-  Transaparent} commands. It is used to fine-tune the strategy for
-unfolding constants, both at the tactic level and at the kernel
-level. This command associates a level to \qualid$_1$ \dots
-\qualid$_n$. Whenever two expressions with two distinct head
-constants are compared (for instance, this comparison can be triggered
-by a type cast), the one with lower level is expanded first. In case
-of a tie, the second one (appearing in the cast type) is expanded.
-
-Levels can be one of the following (higher to lower):
-\begin{description}
-\item[opaque]: level of opaque constants. They cannot be expanded by
-  tactics (behaves like $+\infty$, see next item).
-\item[\num]: levels indexed by an integer. Level $0$ corresponds
-  to the default behaviour, which corresponds to transparent
-  constants. This level can also be referred to as {\bf transparent}.
-  Negative levels correspond to constants to be expanded before normal
-  transparent constants, while positive levels correspond to constants
-  to be expanded after normal transparent constants.
-\item[expand]: level of constants that should be expanded first
-  (behaves like $-\infty$)
-\end{description}
-
-These directives survive section and module closure, unless the
-command is prefixed by {\tt Local}. In the latter case, the behaviour
-regarding sections and modules is the same as for the {\tt
-  Transparent} and {\tt Opaque} commands.
+This commands display all the assumptions (axioms, parameters and
+variables) a theorem or definition depends on.  Especially, it informs
+on the assumptions with respect to which the validity of a theorem
+relies.
 
 \subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}}
 This command displays the name and type of all theorems of the current
@@ -370,7 +297,7 @@ directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a
 graphical environment is also running. The browser to use can be
 selected by setting the environment variable {\tt
 COQREMOTEBROWSER}. If not explicitly set, it defaults to
-\verb!firefox -remote "OpenURL(%s)"!  or
+\verb!firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"!  or
 \verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the
 underlying operating system (in the command, the string \verb!%s!
 serves as metavariable for the url to open).
@@ -477,132 +404,89 @@ successively in each of the directories specified in the {\em
 
 \section[Compiled files]{Compiled files\label{compiled}\index{Compiled files}}
 
-This feature allows to build files for a quick loading. When loaded,
-the commands contained in a compiled file will not be {\em replayed}.
-In particular, proofs will not be replayed. This avoids a useless
-waste of time.
-
-\Rem A module containing an opened section cannot be compiled. 
-
-% \subsection{\tt Compile Module {\ident}.}
-% \index{Modules}
-% \comindex{Compile Module}
-% \index{.vo files}
-% This command loads the file
-% {\ident}{\tt .v} and plays the script it contains. Declarations,
-% definitions and proofs it contains are {\em "packaged"} in a compiled
-% form: the {\em module} named {\ident}.
-% A file {\ident}{\tt .vo} is then created.
-% The file {\ident}{\tt .v} is searched according to the
-% current loadpath.
-% The {\ident}{\tt .vo} is then written in the directory where
-% {\ident}{\tt .v} was found.
-
-% \begin{Variants}
-% \item \texttt{Compile Module {\ident} {\str}.}\\ 
-%   Uses the file {\str}{\tt .v} or {\str} if the previous one does not
-%   exist to build the module {\ident}. In this case, {\str} is any
-%   string giving a filename in the UNIX sense (see section
-%   \ref{Load-str}). 
-%   \Warning The given filename can not contain other caracters than
-%   the caracters of \Coq's identifiers : letters or digits or the
-%   underscore symbol ``\_''.
-
-% \item \texttt{Compile Module Specification {\ident}.}\\
-%   \comindex{Compile Module Specification}
-%   Builds a specification module: only the types of terms are stored
-%   in the module. The bodies (the proofs) are {\em not} written
-%   in the module. In that case, the file created is {\ident}{\tt .vi}.
-%   This is only useful when proof terms take too much place in memory
-%   and are not necessary.
-  
-% \item \texttt{Compile Verbose Module {\ident}.}\\ 
-%   \comindex{Compile Verbose Module}
-%   Verbose version of Compile: shows the contents of the file being
-%   compiled.
-% \end{Variants}
-
-% These different variants can be combined.
-
-
-% \begin{ErrMsgs}
-% \item \texttt{You cannot open a module when there are things other than}\\
-%   \texttt{Modules and Imports in the context.}\\ 
-%   The only commands allowed before a {Compile Module} command are {\tt
-%     Require},\\
-%   {\tt Read Module} and {\tt Import}. Actually, The normal way to
-%   compile modules is by the {\tt coqc} command (see chapter
-%   \ref{Addoc-coqc}).
-% \end{ErrMsgs}
-
-% \SeeAlso sections \ref{Opaque}, \ref{loadpath}, chapter
-% \ref{Addoc-coqc}
-
-%\subsection[\tt Import {\qualid}.]{\tt Import {\qualid}.\comindex{Import}}
-%\label{Import}
+This section describes the commands used to load compiled files (see
+Chapter~\ref{Addoc-coqc} for documentation on how to compile a file).
+A compiled file is a particular case of module called {\em library file}.
 
 %%%%%%%%%%%%
 % Import and Export described in RefMan-mod.tex
 % the minor difference (to avoid multiple Exporting of libraries) in
 % the treatment of normal modules and libraries by Export omitted
 
-
-\subsection[\tt Require {\dirpath}.]{\tt Require {\dirpath}.\label{Require}
+\subsection[\tt Require {\qualid}.]{\tt Require {\qualid}.\label{Require}
 \comindex{Require}}
 
-This command looks in the loadpath for a file containing module
-{\dirpath}, then loads and opens (imports) its contents.
-More precisely, if {\dirpath} splits into a library dirpath {\dirpath'} and a module name {\textsl{ident}}, then the file {\ident}{\tt .vo} is searched in a physical path mapped to the logical path {\dirpath'}.
+This command looks in the loadpath for a file containing
+module {\qualid} and adds the corresponding module to the environment
+of {\Coq}. As library files have dependencies in other library files,
+the command {\tt Require {\qualid}} recursively requires all library
+files the module {\qualid} depends on and adds the corresponding modules to the
+environment of {\Coq} too. {\Coq} assumes that the compiled files have
+been produced by a valid {\Coq} compiler and their contents are then not
+replayed nor rechecked.
+
+To locate the file in the file system, {\qualid} is decomposed under
+the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt
+.vo} is searched in the directory of the physical file system that is
+mapped in {\Coq} loadpath to the logical path {\dirpath} (see
+Section~\ref{Loadpath}).
+
+\begin{Variants}
+\item {\tt Require Import {\qualid}.}\\ \comindex{Require} 
 
-TODO: effect on the name table.
+  This loads and declares the module {\qualid} and its dependencies
+  then imports the contents of {\qualid} as described in
+  Section~\ref{Import}.
 
-% The implementation file ({\ident}{\tt .vo}) is searched first,
-% then the specification file ({\ident}{\tt .vi}) in case of failure.
-If the module required has already been loaded, \Coq\ 
-simply opens it (as {\tt Import {\dirpath}} would do it).
-%If the module required is already loaded and open, \Coq\ 
-%displays the following warning: {\tt {\ident} already imported}.
+  It does not import the modules on which {\qualid} depends unless
+  these modules were itself required in module {\qualid} using {\tt
+  Require Export}, as described below, or recursively required through
+  a sequence of {\tt Require Export}.
 
-If a module {\it A} contains a command {\tt Require} {\it B} then the
-command {\tt Require} {\it A} loads the module {\it B} but does not
-open it (See the {\tt Require Export} variant below).
+  If the module required has already been loaded, {\tt Require Import
+  {\qualid}} simply imports it, as {\tt Import {\qualid}} would.
 
-\begin{Variants}
-\item {\tt Require Export {\qualid}.}\\
+\item {\tt Require Export {\qualid}.}
   \comindex{Require Export}
-  This command acts as {\tt Require} {\qualid}.  But if a module {\it
-    A} contains a command {\tt Require Export} {\it B}, then the
-  command {\tt Require} {\it A} opens the module {\it B} as if the
-  user would have typed {\tt Require}{\it B}.
-% \item {\tt Require $[$ Implementation $|$ Specification $]$ {\qualid}.}\\
-%   \comindex{Require Implementation}
-%   \comindex{Require Specification}
-%   Is the same as {\tt Require}, but specifying explicitly the
-%   implementation ({\tt.vo} file) or the specification ({\tt.vi}
-%   file).
-
-% Redundant ?
-% \item {\tt Require {\qualid} {\str}.}\\ 
-%   Specifies the file to load as being {\str} but containing module
-%  {\qualid}. 
-% The opened module is still {\ident} and therefore must have been loaded.
-\item {\tt Require {\qualid} {\str}.}\\ 
-  Specifies the file to load as being {\str} but containing module
-  {\qualid} which is then opened.
-\end{Variants}
 
-These different variants can be combined.
+  This command acts as {\tt Require Import} {\qualid}, but if a
+  further module, say {\it A}, contains a command {\tt Require
+  Export} {\it B}, then the command {\tt Require Import} {\it A}
+  also imports the module {\it B}.
+
+\item {\tt Require \zeroone{Import {\sl |} Export} {\qualid}$_1$ \ldots {\qualid}$_n$.}
+
+  This loads the modules {\qualid}$_1$, \ldots, {\qualid}$_n$ and
+  their recursive dependencies. If {\tt Import} or {\tt Export} is
+  given, it also imports {\qualid}$_1$, \ldots, {\qualid}$_n$ and all
+  the recursive dependencies that were marked or transitively marked
+  as {\tt Export}.
+
+\item {\tt Require \zeroone{Import {\sl |} Export} {\str}.}
+
+  This shortcuts the resolution of the qualified name into a library
+  file name by directly requiring the module to be found in file
+  {\str}.vo.
+\end{Variants}
 
 \begin{ErrMsgs}
 
-\item \errindex{Cannot load {\ident}: no physical path bound to {\dirpath}}
+\item \errindex{Cannot load {\qualid}: no physical path bound to {\dirpath}}
 
-\item \errindex{Can't find module toto on loadpath}
+\item \errindex{Cannot find library foo in loadpath}
 
-  The command did not find the file {\tt toto.vo}. Either {\tt
-    toto.v} exists but is not compiled or {\tt toto.vo} is in a directory
+  The command did not find the file {\tt foo.vo}. Either {\tt
+    foo.v} exists but is not compiled or {\tt foo.vo} is in a directory
   which is not in your {\tt LoadPath} (see Section~\ref{loadpath}).
 
+\item \errindex{Compiled library {\ident}.vo makes inconsistent assumptions over library {\qualid}}
+
+  The command tried to load library file {\ident}.vo that depends on
+  some specific version of library {\qualid} which is not the one
+  already loaded in the current {\Coq} session. Probably {\ident}.v
+  was not properly recompiled with the last version of the file
+  containing module {\qualid}.
+
 \item \errindex{Bad magic number}
 
   \index{Bad-magic-number@{\tt Bad Magic Number}}
@@ -614,8 +498,10 @@ These different variants can be combined.
 \SeeAlso Chapter~\ref{Addoc-coqc}
 
 \subsection[\tt Print Libraries.]{\tt Print Libraries.\comindex{Print Libraries}}
-This command shows the currently loaded (required) and currently
-imported libraries.
+
+This command displays the list of library files loaded in the current
+{\Coq} session. For each of these libraries, it also tells if it is
+imported.
 
 \subsection[\tt Declare ML Module {\str$_1$} .. {\str$_n$}.]{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.\comindex{Declare ML Module}}
 This commands loads the Objective Caml compiled files {\str$_1$} \dots
@@ -760,7 +646,7 @@ environment (see Chapter~\ref{Proof-handling}). The three numbers
 $\num_1$, $\num_2$ and $\num_3$ represent the following:
 \begin{itemize}
 \item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number
-  of currently opened nested proofs that must be cancelled (see
+  of currently opened nested proofs that must be canceled (see
   Chapter~\ref{Proof-handling}).
 \item $\num_2$: \emph{Proof state number} to unbury once aborts have
   been done. Coq will compute the number of \texttt{Undo} to perform
@@ -804,7 +690,7 @@ suppose the current prompt is:
 \verb!|!goal1\verb!|!goal4\verb!|!goal3\verb!|!goal2\verb!|! 
 \verb!|!8 \verb!< </prompt>!
 
-and we want to backtrack to a state labelled by:
+and we want to backtrack to a state labeled by:
 
 \verb!<! goal2 \verb!<! 32
 \verb!|!goal1\verb!|!goal2
@@ -865,7 +751,7 @@ Objective Caml toplevel. The Objective Caml command:
 \end{flushleft}
 
 \noindent add the right loadpaths and loads some toplevel printers for
-all abstract types of \Coq - section\_path, identfifiers, terms, judgements,
+all abstract types of \Coq - section\_path, identifiers, terms, judgments,
 \dots. You can also use the file \texttt{base\_include} instead,
 that loads only the pretty-printers for section\_paths and
 identifiers.
@@ -887,7 +773,7 @@ go();;
 
 \subsection[\tt Time \textrm{\textsl{command}}.]{\tt Time \textrm{\textsl{command}}.\comindex{Time}
 \label{time}}
-This command executes the vernac command \textrm{\textsl{command}}
+This command executes the vernacular command \textrm{\textsl{command}}
 and display the time needed to execute it.
 
 \section{Controlling display}
@@ -933,17 +819,100 @@ This command displays the current nesting depth used for display.
 %\subsection{\tt Abstraction ...}
 %Not yet documented.
 
-\section{Controlling the conversion algorithm}
+\section{Controlling the reduction strategies and the conversion algorithm}
 
-{\Coq} comes with two algorithms to check the convertibility of types
-(see Section~\ref{convertibility}). The first algorithm lazily
+{\Coq} provides reduction strategies that the tactics can invoke and
+two different algorithms to check the convertibility of types.
+The first conversion algorithm lazily
 compares applicative terms while the other is a brute-force but efficient
 algorithm that first normalizes the terms before comparing them.  The
 second algorithm is based on a bytecode representation of terms
 similar to the bytecode representation used in the ZINC virtual
 machine~\cite{Leroy90}. It is specially useful for intensive
 computation of algebraic values, such as numbers, and for reflexion-based
-tactics.
+tactics. The commands to fine-tune the reduction strategies and the
+lazy conversion algorithm are described first.
+
+\subsection[\tt Opaque \qualid$_1$ \dots \qualid$_n$.]{\tt Opaque \qualid$_1$ \dots \qualid$_n$.\comindex{Opaque}\label{Opaque}} This command tells not to unfold
+the constants {\qualid$_1$} \dots {\qualid$_n$} in tactics using
+$\delta$-conversion. Unfolding a constant is replacing it by its
+definition. {\tt Opaque} can only apply on constants originally
+defined as {\tt Transparent}.
+
+Constants defined by a proof ended by {\tt Qed} are automatically
+stamped as {\tt Opaque} and can no longer be considered as {\tt
+Transparent}. This is to keep with the usual mathematical practice of
+{\em proof irrelevance}: what matters in a mathematical development is
+the sequence of lemma statements, not their actual proofs. This
+distinguishes lemmas from the usual defined constants, whose actual
+values are of course relevant in general.
+
+\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
+\ref{Theorem}
+
+\begin{ErrMsgs}
+\item \errindex{The reference \qualid\ was not found in the current
+environment}\\
+    There is no constant referred by {\qualid} in the environment.
+    Nevertheless, if you asked \texttt{Opaque foo bar}
+    and if \texttt{bar} does not exist, \texttt{foo} is set opaque.
+\end{ErrMsgs}
+
+\subsection[\tt Transparent \qualid$_1$ \dots \qualid$_n$.]{\tt Transparent \qualid$_1$ \dots \qualid$_n$.\comindex{Transparent}\label{Transparent}}
+This command is the converse of {\tt Opaque} and can only apply on constants originally defined as {\tt Transparent} to restore their initial behavior after an {\tt Opaque} command.
+
+The constants automatically declared transparent are the ones defined by a proof ended by {\tt Defined}, or by a {\tt
+  Definition} or {\tt Local} with an explicit body.
+
+\Warning {\tt Transparent} and \texttt{Opaque} are not synchronous
+with the reset mechanism. If a constant was transparent at point A, if
+you set it opaque at point B and reset to point A, you return to state
+of point A with the difference that the constant is still opaque. This
+can cause changes in tactic scripts behavior.
+
+At section or module closing, a constant recovers the status it got at
+the time of its definition.
+
+\begin{ErrMsgs}
+% \item \errindex{Can not set transparent.}\\
+%     It is a constant from a required module or a parameter.
+\item \errindex{The reference \qualid\ was not found in the current
+environment}\\
+    There is no constant referred by {\qualid} in the environment.
+\end{ErrMsgs}
+
+\SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
+\ref{Theorem}
+
+\subsection{\tt Strategy {\it level} [ \qualid$_1$ \dots \qualid$_n$
+  ].\comindex{Strategy}\comindex{Local Strategy}\label{Strategy}}
+This command generalizes the behavior of {\tt Opaque} and {\tt
+  Transparent} commands. It is used to fine-tune the strategy for
+unfolding constants, both at the tactic level and at the kernel
+level. This command associates a level to \qualid$_1$ \dots
+\qualid$_n$. Whenever two expressions with two distinct head
+constants are compared (for instance, this comparison can be triggered
+by a type cast), the one with lower level is expanded first. In case
+of a tie, the second one (appearing in the cast type) is expanded.
+
+Levels can be one of the following (higher to lower):
+\begin{description}
+\item[opaque]: level of opaque constants. They cannot be expanded by
+  tactics (behaves like $+\infty$, see next item).
+\item[\num]: levels indexed by an integer. Level $0$ corresponds
+  to the default behavior, which corresponds to transparent
+  constants. This level can also be referred to as {\bf transparent}.
+  Negative levels correspond to constants to be expanded before normal
+  transparent constants, while positive levels correspond to constants
+  to be expanded after normal transparent constants.
+\item[expand]: level of constants that should be expanded first
+  (behaves like $-\infty$)
+\end{description}
+
+These directives survive section and module closure, unless the
+command is prefixed by {\tt Local}. In the latter case, the behavior
+regarding sections and modules is the same as for the {\tt
+  Transparent} and {\tt Opaque} commands.
 
 \subsection{\tt Set Virtual Machine
 \label{SetVirtualMachine}
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 761c44b71e..c7f6bf02e7 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -615,7 +615,7 @@ Grégoire and Laurent Théry contributed a modular library for building
 arbitrarily large integers from bounded integers while Evgeny Makarov
 contributed a modular library of abstract natural and integer
 arithmetics together with a few convenient tactics. On his side,
-Pierre Letouzey made various extensions to the arithmetic libraries on
+Pierre Letouzey made numerous extensions to the arithmetic libraries on
 $\mathbb{Z}$ and $\mathbb{Q}$, including extra support for
 automatization in presence of various number-theory concepts.
 
@@ -687,7 +687,7 @@ Foundations group at Radbout university in Nijmegen, reporters of bugs
 and participants to the Coq-Club mailing list.
 
 \begin{flushright}
-Palaiseau, May 2008\\
+Palaiseau, June 2008\\
 Hugo Herbelin\\
 \end{flushright}
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 45993dd230..ffee048d12 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -733,35 +733,6 @@ This tactic applies to any goal. It implements the rule
 \end{Variants}
 
 \SeeAlso \ref{Conversion-tactics}
-\subsection{\tt evar (\ident:\term)
-\tacindex{evar}
-\label{evar}}
-
-The {\tt evar} tactic creates a new local definition named \ident\ with
-type \term\ in the context. The body of this binding is a fresh
-existential variable.
-
-\subsection{\tt instantiate (\num:= \term)
-\tacindex{instantiate}
-\label{instantiate}}
-
-The {\tt instantiate} tactic allows to solve an existential variable
-with the term \term. The \num\  argument is the position of the
-existential variable from right to left in the conclusion. This cannot be
-the number of the existential variable since this number is different
-in every session.
-
-\begin{Variants}
-  \item {\tt instantiate (\num:=\term) in \ident}
-  
-  \item {\tt instantiate (\num:=\term) in (Value of \ident)}
-  
-  \item {\tt instantiate (\num:=\term) in (Type of \ident)}
-
-These allow to refer respectively to existential variables occurring in 
-a hypothesis or in the body or the type of a local definition.  
-
-\end{Variants}
 
 \subsection{\tt fix {\ident} {\num}
 \tacindex{fix}
@@ -834,6 +805,48 @@ simultaneously proved are respectively {\tt forall}
 
 \end{Variants}
 
+\subsection{\tt evar (\ident:\term)
+\tacindex{evar}
+\label{evar}}
+
+The {\tt evar} tactic creates a new local definition named \ident\ with
+type \term\ in the context. The body of this binding is a fresh
+existential variable.
+
+\subsection{\tt instantiate (\num:= \term)
+\tacindex{instantiate}
+\label{instantiate}}
+
+The {\tt instantiate} tactic allows to solve an existential variable
+with the term \term. The \num\  argument is the position of the
+existential variable from right to left in the conclusion. This cannot be
+the number of the existential variable since this number is different
+in every session.
+
+\begin{Variants}
+  \item {\tt instantiate (\num:=\term) in \ident}
+  
+  \item {\tt instantiate (\num:=\term) in (Value of \ident)}
+  
+  \item {\tt instantiate (\num:=\term) in (Type of \ident)}
+
+These allow to refer respectively to existential variables occurring in 
+a hypothesis or in the body or the type of a local definition.  
+
+\end{Variants}
+
+\subsection{Bindings list
+\tacindex{admit}
+\label{admit}}
+
+The {\tt admit} tactic ``solves'' the current subgoal by an
+axiom. This typically allows to temporarily skip a subgoal so as to
+progress further in the rest of the proof. To know if some proof still
+relies on unproved subgoals, one can use the command {\tt Print
+Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals
+have names of the form {\ident}\texttt{\_admitted} possibly followed
+by a number.
+
 \subsection{Bindings list
 \index{Binding list}
 \label{Binding-list}}
@@ -1389,10 +1402,11 @@ equivalent to {\tt intros; apply ci}.
 
 \end{Variants}
 
-\section[Eliminations (Induction and Case Analysis)]{Eliminations (Induction and Case Analysis)\label{Tac-induction}}
-Elimination tactics are useful to prove statements by induction or
-case analysis.  Indeed, they make use of the elimination (or
-induction) principles generated with inductive definitions (see
+\section[Induction and Case Analysis]{Induction and Case Analysis
+\label{Tac-induction}}
+
+The tactics presented in this section implement induction or case
+analysis on inductive or coinductive objects (see
 Section~\ref{Cic-inductive-definitions}).
 
 \subsection{\tt induction \term
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 73fc878b41..afef3b41ae 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -557,7 +557,7 @@ type backtrack =
 | NoBacktrack
 
 let add_undo (n,a,b) = (n+1,a,b)
-let add_abort (n,a,b) = (n,a+1,b)
+let add_abort (n,a,b) = (0,a+1,b)
 let add_backtrack (n,a,b) b' = (n,a,b')
 
 let pop_command undos t =
@@ -598,16 +598,16 @@ let rec apply_backtrack = function
         end
 
 let rec apply_undos (n,a,b) =
+  (* Aborts *)
+  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
+  (try Util.repeat a Pfedit.delete_current_proof ()
+   with e -> prerr_endline "WARNING : found a closed environment"; raise e);
   (* Undos *)
   if n<>0 then 
     (prerr_endline ("Applying "^string_of_int n^" undos");
      try Pfedit.undo n
-     with _ -> apply_undos (n,a,BacktrackToNextActiveMark));
-  (* Aborts *)
-  if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts");
-  (try Util.repeat a Pfedit.delete_current_proof ()
-   with e ->
-     begin prerr_endline "WARNING : found a closed environment"; raise e end);
+     with _ -> (* Undo stack exhausted *)
+       apply_backtrack BacktrackToNextActiveMark);
   (* Reset *)
   apply_backtrack b
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 0635ad7c1f..dbb8c38abf 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -129,4 +129,4 @@ let browser_cmd_fmt =
   Not_found ->
    if Sys.os_type = "Win32"
    then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s"
-   else "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s"
+   else "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"
diff --git a/library/library.ml b/library/library.ml
index c014865fe5..e595df092c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -122,7 +122,6 @@ type library_disk = {
 
 type library_t = {
   library_name : compilation_unit_name;
-  library_filename : System.physical_path;
   library_compiled : compiled_library;
   library_objects : library_objects;
   library_deps : (compilation_unit_name * Digest.t) list;
@@ -138,10 +137,15 @@ module LibraryOrdered =
   end
 
 module LibraryMap = Map.Make(LibraryOrdered)
+module LibraryFilenameMap = Map.Make(LibraryOrdered)
 
 (* This is a map from names to loaded libraries *)
 let libraries_table = ref LibraryMap.empty
 
+(* This is the map of loaded libraries filename *)
+(* (not synchronized so as not to be caught in the states on disk) *)
+let libraries_filename_table = ref LibraryFilenameMap.empty
+
 (* These are the _ordered_ sets of loaded, imported and exported libraries *)
 let libraries_loaded_list = ref []
 let libraries_imports_list = ref []
@@ -175,6 +179,9 @@ let _ =
 
 (* various requests to the tables *)
 
+let exists_library dir =
+  LibraryMap.mem dir !libraries_table
+
 let find_library dir =
   LibraryMap.find dir !libraries_table
 
@@ -183,7 +190,15 @@ let try_find_library dir =
   with Not_found ->
     error ("Unknown library " ^ (string_of_dirpath dir))
 
-let library_full_filename dir = (find_library dir).library_filename
+let register_library_filename dir f =
+  (* Not synchronized: overwrite the previous binding if one existed *)
+  (* from a previous play of the session *)
+  libraries_filename_table := 
+    LibraryFilenameMap.add dir f !libraries_filename_table
+
+let library_full_filename dir =
+  try LibraryFilenameMap.find dir !libraries_filename_table
+  with Not_found -> "unavailable"
 
 let library_is_loaded dir =
   try let _ = find_library dir in true
@@ -309,7 +324,7 @@ let with_magic_number_check f a =
   try f a
   with System.Bad_magic_number fname ->
     errorlabstrm "with_magic_number_check"
-    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
+    (str"File " ++ str fname ++ spc () ++ str"has bad magic number." ++
     spc () ++ str"It is corrupted" ++ spc () ++
     str"or was compiled with another version of Coq.")
 
@@ -351,10 +366,9 @@ let locate_qualified_library qid =
     let path, file = System.where_in_path loadpath name in
     let dir = extend_dirpath (find_logical_path path) base in
     (* Look if loaded *)
-    try 
-      (LibLoaded, dir, library_full_filename dir)      
-    with Not_found ->
-      (LibInPath, dir, file)
+    if exists_library dir then (LibLoaded, dir, library_full_filename dir)
+    (* Otherwise, look for it in the file system *)
+    else (LibInPath, dir, file)
   with Not_found -> raise LibNotFound
 
 let explain_locate_library_error qid = function
@@ -388,9 +402,8 @@ let try_locate_qualified_library (loc,qid) =
 let lighten_library m = 
   if !Flags.dont_load_proofs then lighten_library m else m
 
-let mk_library md f digest = {
+let mk_library md digest = {
   library_name = md.md_name;
-  library_filename = f;
   library_compiled = lighten_library md.md_compiled;
   library_objects = md.md_objects;
   library_deps = md.md_deps;
@@ -402,7 +415,8 @@ let intern_from_file f =
   let md = System.marshal_in ch in
   let digest = System.marshal_in ch in
   close_in ch;
-  mk_library md f digest
+  register_library_filename md.md_name f;
+  mk_library md digest
 
 let rec intern_library needed (dir, f) =
   (* Look if in the current logical environment *)
@@ -426,9 +440,9 @@ and intern_library_deps needed dir m =
 and intern_mandatory_library caller needed (dir,d) =
   let m,needed = intern_library needed (try_locate_absolute_library dir) in
   if d <> m.library_digest then
-    error ("compiled library "^(string_of_dirpath caller)^
-	   " makes inconsistent assumptions over library "
-	   ^(string_of_dirpath dir));
+    errorlabstrm "" (strbrk ("Compiled library "^(string_of_dirpath caller)^
+	   ".vo makes inconsistent assumptions over library "
+	   ^(string_of_dirpath dir)));
   needed
 
 let rec_intern_library needed mref =
@@ -443,17 +457,18 @@ let check_library_short_name f dir = function
   | _ -> ()
 
 let rec_intern_by_filename_only id f =
-  let m = intern_from_file f in
+  let m = try intern_from_file f with Sys_error s -> error s in
   (* Only the base name is expected to match *)
   check_library_short_name f m.library_name id;
   (* We check no other file containing same library is loaded *)
-  try
-    let m' = find_library m.library_name in
-    Flags.if_verbose warning 
-      ((string_of_dirpath m.library_name)^" is already loaded from file "^
-       m'.library_filename);
-    m.library_name, []
-  with Not_found ->
+  if exists_library m.library_name then
+    begin
+      Flags.if_verbose warning 
+	((string_of_dirpath m.library_name)^" is already loaded from file "^
+	library_full_filename m.library_name);
+      m.library_name, []
+    end
+ else
     let needed = intern_library_deps [] m.library_name m in
     m.library_name, needed
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 795627fc41..8b32224d2d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -92,10 +92,12 @@ let retype sigma metamap =
           | Prop _, (Prop Pos as s) -> s
           | Type _, (Prop Pos as s) when
               Environ.engagement env = Some ImpredicativeSet -> s
+	  | (Type _, _) | (_, Type _) -> new_Type_sort ()
+(*
           | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ)
 	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
 	  | Prop Null, (Type _ as s) -> s
-	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
+	  | Type u1, Type u2 -> Type (Univ.sup u1 u2)*))
     | App(f,args) when isGlobalRef f ->
 	let t = type_of_global_reference_knowing_parameters env f args in
         sort_of_atomic_type env sigma t args
diff --git a/test-suite/bugs/closed/shouldsucceed/1865.v b/test-suite/bugs/closed/shouldsucceed/1865.v
new file mode 100644
index 0000000000..17c1998948
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1865.v
@@ -0,0 +1,18 @@
+(* Check that tactics (here dependent inversion) do not generate
+   conversion problems T <= U with sup's of universes in U *)
+
+(* Submitted by David Nowak *)
+
+Inductive list (A:Set) : nat -> Set :=
+| nil : list A O
+| cons : forall n, A -> list A n -> list A (S n).
+
+Definition f (n:nat) : Type :=
+  match n with
+  | O => bool
+  | _ => unit
+  end.
+
+Goal forall A n, list A n -> f n.
+intros A n.
+dependent inversion n.