MAJ et bricoles diverses

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

6 files changed, 30 insertions, 8 deletions

diff --git a/CHANGES b/CHANGES
index a349979fc..1303bc4b5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,7 +63,6 @@ Libraries (DOC TO CHECK)
   elements, nothing more). 
 - In ListSet, a few definitions are now in Type (may induce a few
   incompatibilities).
-- Notation [t;...;u] for lists made available in list_scope.
 - Changes in FSets/FMaps:
   - Improvements: in particular FMap now provides an induction principle 
     on maps, and some properties about FSets and fold needs less hypotheses.
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 9f607f05e..71e87b3f3 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -994,10 +994,10 @@ syntax
 
 \noindent
 \begin{tabular}{lcl}
-{\sentence} & ::= & \texttt{Tactic Notation} {\taclevel} \sequence{\proditem}{} \\
+{\sentence} & ::= & \texttt{Tactic Notation} \zeroone{\taclevel} \nelist{\proditem}{} \\
 & & \texttt{:= {\tac} .}\\
 {\proditem} & ::= & {\str} $|$ {\tacargtype}{\tt ({\ident})} \\ 
-{\taclevel} & ::= & $|$ {\tt (at level} {\naturalnumber}{\tt )} \\
+{\taclevel} & ::= & {\tt (at level} {\naturalnumber}{\tt )} \\
 {\tacargtype} & ::= &
 %{\tt preident} $|$
 {\tt ident} $|$
@@ -1007,9 +1007,9 @@ syntax
 {\tt reference} $|$
 {\tt constr} \\ & $|$ &
 %{\tt castedopenconstr} $|$
-{\tt integer} \\ & $|$ &
-{\tt int\_or\_var} $|$
-{\tt tactic} $|$
+{\tt integer} $|$
+{\tt int\_or\_var} \\ & $|$ &
+{\tt tactic} $|$ {\tt tactic$n$} \qquad\mbox{(for $0\leq n\leq 5$)}
 \end{tabular}
 \medskip
 
@@ -1021,7 +1021,8 @@ production items. It then evaluates into the tactic expression
 symbol, i.e. a {\str}, for the first production item.  The tactic
 level indicates the parsing precedence of the tactic notation. This
 information is particularly relevant for notations of tacticals.
-Levels 0 to 5 are available. To know the parsing precedences of the
+Levels 0 to 5 are available (default is 0). 
+To know the parsing precedences of the
 existing tacticals, use the command {\tt Print Grammar tactic.}
 
 Each type of tactic argument has a specific semantic regarding how it
@@ -1045,7 +1046,8 @@ Tactic argument type & parsed as & interpreted as & as in tactic \\
 %%{\tt\small castedopenconstr} & term & a term with its sign. of exist. var. & {\tt refine}\\
 {\tt\small integer} & integer & an integer &  \\
 {\tt\small int\_or\_var} & identifier or integer & an integer & {\tt do} \\
-{\tt\small tactic} & tactic & a tactic & \\
+{\tt\small tactic} & tactic at level 5 & a tactic & \\
+{\tt\small tactic$n$} & tactic at level $n$ & a tactic & \\
 \end{tabular}
 
 \Rem In order to be bound in tactic definitions, each syntactic entry
diff --git a/test-suite/check b/test-suite/check
index d01f9b51a..4c98f8ac2 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -106,6 +106,7 @@ test_interactive() {
 # La fonction suivante teste en interactif 
 # It expects a line "(* Expected time < XXX.YYs *)" in the .v file 
 # with exactly two digits after the dot
+# The reference for time is a 6120 bogomips cpu
 test_complexity() {
     if [ -f /proc/cpuinfo ]; then
 	if grep -q bogomips /proc/cpuinfo; then # i386, ppc
diff --git a/test-suite/complexity/ring.v b/test-suite/complexity/ring.v
new file mode 100644
index 000000000..5a541bc24
--- /dev/null
+++ b/test-suite/complexity/ring.v
@@ -0,0 +1,7 @@
+(* This example, checks the efficiency of the abstract machine used by ring *)
+(* Expected time < 1.00s *)
+
+Require Import ZArith.
+Open Scope Z_scope.
+Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
+Time intro; ring.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 4f642a73e..2244e1b9a 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -115,6 +115,9 @@ Proof. destruct 1 as (x,H); exists x; trivial. Defined.
 Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P.
 Proof. destruct 1 as (x,H); exists x; trivial. Defined.
 
+Coercion sigT_of_sig : sig >-> sigT.
+Coercion sig_of_sigT : sigT >-> sig.
+
 (** [sumbool] is a boolean type equipped with the justification of
     their value *)
 
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
index 5bdbb76b9..357e5e212 100644
--- a/theories/Reals/Rpow_def.v
+++ b/theories/Reals/Rpow_def.v
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
 Require Import Rdefinitions.
 
 Fixpoint pow (r:R) (n:nat) {struct n} : R :=