*** empty log message ***

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

10 files changed, 108 insertions, 85 deletions

diff --git a/CHANGES b/CHANGES
index 402771b33..7d5f7dbce 100644
--- a/CHANGES
+++ b/CHANGES
@@ -165,7 +165,7 @@ Tactic language
 
 - Fail tactic now accepts a failure message
 - Idtac tactic now accepts a message
-- New primitive tactic "FreshId" (new syntax: "Fresh") to generate new names
+- New primitive tactic "FreshId" (new syntax: "fresh") to generate new names
 - Debugger prints levels of calls
 
 Tactics
@@ -195,6 +195,8 @@ Tactics
   immediate hint), resulting in shorter proofs
 - Instantiate now works in hyps (syntax : Instantiate in ...)
 - Some new tactics : EConstructor, ELeft, Eright, ESplit, EExists
+- Clear now fails when trying to remove a local definition used by
+  a constant appearing in the current goal
 
 Extraction (See details in contrib/extraction/CHANGES)
 
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index d6f76a0a9..bfdf5dbfc 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -90,6 +90,7 @@ TACTIC EXTEND Firstorder
       [ gen_ground_tac true (option_app eval_tactic t) Void ]
 END
 
+(* Obsolete since V8.0
 TACTIC EXTEND GTauto   
   [ "GTauto" ] ->
      [ gen_ground_tac false (Some fail_solver) Void ]   
@@ -99,4 +100,4 @@ TACTIC EXTEND GIntuition
   [ "GIntuition" tactic_opt(t) ] ->
      [ gen_ground_tac false (option_app eval_tactic t) Void ]
 END
-
+*)
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 354222a15..91ca74ddc 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -103,7 +103,9 @@ Lexical categories are:
 \SEPDEF
 \DEFNT{meta-ident}  \CHAR{?}\NT{ident}   
 \SEPDEF
-\DEFNT{int}         \PLUS{\NT{digit}}
+\DEFNT{num}         \PLUS{\NT{digit}}
+\SEPDEF
+\DEFNT{int}         \NT{num} \mid \CHAR{-}\NT{num}
 \SEPDEF
 \DEFNT{digit}       \CHAR{0}-\CHAR{9}
 \SEPDEF
@@ -186,26 +188,26 @@ conflict can appear, $\NTL{constr}{200}$ is also used as entry point.
 \nlsep \KWD{fun} ~\NT{binder-list} ~\KWD{$\Rightarrow$}~\NTL{constr}{200}
           &&\RNAME{lambda}
 \nlsep \NT{fix-expr}
-\nlsep \KWD{let}~\NT{ident}~\STAR{\NT{binder-let}}~\NT{type-cstr}
-       ~\KWD{:=}~\NTL{constr}{200}
+\nlsep \KWD{let}~\NT{ident-with-params} ~\KWD{:=}~\NTL{constr}{200}
        ~\KWD{in}~\NTL{constr}{200}  &&\RNAME{let}
 \nlsep \KWD{let}~\NT{single-fix} ~\KWD{in}~\NTL{constr}{200}
           &&\RNAME{rec-let}
 \nlsep \KWD{let}~\KWD{(}~\OPT{\NT{let-pattern}}~\KWD{)}~\OPT{\NT{return-type}}
        ~\KWD{:=}~\NTL{constr}{200}~\KWD{in}~\NTL{constr}{200}
           &&\RNAME{let-case}
-\nlsep \KWD{if}~\NT{constr}~\OPT{\NT{return-type}}
+\nlsep \KWD{if}~\NT{if-item}
        ~\KWD{then}~\NTL{constr}{200}~\KWD{else}~\NTL{constr}{200}
           &&\RNAME{if-case}
 \SEPDEF
 \DEFNT{appl-arg}
        \KWD{(}~\NT{ident}~\!\KWD{:=}~\NTL{constr}{200}~\KWD{)}  &&\RNAME{impl-arg}
+       \KWD{(}~\NT{num}~\!\KWD{:=}~\NTL{constr}{200}~\KWD{)}  &&\RNAME{impl-arg}
 \nlsep \NTL{constr}{9}
 \SEPDEF
 \DEFNT{atomic-constr}
        \NT{reference}     && \RNAME{variables}
 \nlsep \NT{sort}          && \RNAME{CIC-sort}
-\nlsep \NT{int}           && \RNAME{number}
+\nlsep \NT{num}           && \RNAME{number}
 \nlsep \KWD{_}            && \RNAME{hole}
 \nlsep \NT{meta-ident}    && \RNAME{meta/evar}
 \end{rules}
@@ -213,6 +215,9 @@ conflict can appear, $\NTL{constr}{200}$ is also used as entry point.
 
 
 \begin{rules}
+\DEFNT{ident-with-params}
+       \NT{ident}~\STAR{\NT{binder-let}}~\NT{type-cstr}
+\SEPDEF
 \DEFNT{binder-list}
        \NT{binder}~\STAR{\NT{binder-let}}
 \nlsep \PLUS{\NT{name}}~\KWD{:}~\NT{constr}
@@ -266,22 +271,22 @@ conflict can appear, $\NTL{constr}{200}$ is also used as entry point.
 
 \begin{rules}
 \DEFNT{match-expr}
-       \KWD{match}~\NT{case-items}~\OPT{\NT{case-type}}~\KWD{with}
+       \KWD{match}~\NT{match-items}~\OPT{\NT{return-type}}~\KWD{with}
   ~\OPT{\TERMbar}~\OPT{\NT{branches}}~\KWD{end}        &&\RNAME{match}
 \SEPDEF
-\DEFNT{case-items}
-       \NT{case-item} ~\KWD{,} ~\NT{case-items}
-\nlsep \NT{case-item}
+\DEFNT{match-items}
+       \NT{match-item} ~\KWD{,} ~\NT{match-items}
+\nlsep \NT{match-item}
 \SEPDEF
-\DEFNT{case-item}
+\DEFNT{match-item}
        \NTL{constr}{100}~\OPTGR{\KWD{as}~\NT{name}}
        ~\OPTGR{\KWD{in}~\NTL{constr}{100}}
 \SEPDEF
-\DEFNT{case-type}
+\DEFNT{return-type}
        \KWD{return}~\NTL{constr}{100}
 \SEPDEF
-\DEFNT{return-type}
-       \OPTGR{\KWD{as}~\NT{name}}~\NT{case-type}
+\DEFNT{if-item}
+       \NT{constr}~\OPTGR{\OPTGR{\KWD{as}~\NT{name}}~\NT{return-type}}
 \SEPDEF
 \DEFNT{branches}
        \NT{eqn}~\TERMbar~\NT{branches}
@@ -297,7 +302,7 @@ conflict can appear, $\NTL{constr}{200}$ is also used as entry point.
 \nlsep \NT{pattern}~\KWD{\%}~\NT{ident}    &1L & \RNAME{scope-change}
 \nlsep \NT{reference}                      &0  & \RNAME{pattern-var}
 \nlsep \KWD{_}                             &0  & \RNAME{hole}
-\nlsep \NT{int}                            &0
+\nlsep \NT{num}                            &0
 \nlsep \KWD{(}~\NT{tuple-pattern}~\KWD{)}
 \SEPDEF
 \DEFNT{tuple-pattern}
@@ -397,8 +402,8 @@ $$
 \nlsep \TERM{elimtype}~\tacconstr
 \nlsep \TERM{case}~\NT{constr-with-bindings}
 \nlsep \TERM{casetype}~\tacconstr
-\nlsep \KWD{fix}~\OPT{\NT{ident}}~\NT{int}
-\nlsep \KWD{fix}~\NT{ident}~\NT{int}~\KWD{with}~\PLUS{\NT{fix-spec}}
+\nlsep \KWD{fix}~\OPT{\NT{ident}}~\NT{num}
+\nlsep \KWD{fix}~\NT{ident}~\NT{num}~\KWD{with}~\PLUS{\NT{fix-spec}}
 \nlsep \KWD{cofix}~\OPT{\NT{ident}}
 \nlsep \KWD{cofix}~\NT{ident}~\PLUS{\NT{fix-spec}}
 %%
@@ -416,9 +421,9 @@ $$
 \nlsep \TERM{set}~
   \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}}
 \nlsep \TERM{instantiate}~
-  \TERM{(}~\NT{int}~\TERM{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}}
+  \TERM{(}~\NT{num}~\TERM{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}}
 %%
-\nlsep \TERM{specialize}~\OPT{\NT{int}}~\NT{constr-with-bindings}
+\nlsep \TERM{specialize}~\OPT{\NT{num}}~\NT{constr-with-bindings}
 \nlsep \TERM{lapply}~\tacconstr
 %%
 \nlsep \TERM{simple}~\TERM{induction}~\NT{quantified-hyp}
@@ -439,14 +444,14 @@ $$
 \begin{rules}
 \EXTNT{simple-tactic}
        \TERM{trivial}~\OPT{\NT{hint-bases}}
-\nlsep \TERM{auto}~\OPT{\NT{int}}~\OPT{\NT{hint-bases}}
+\nlsep \TERM{auto}~\OPT{\NT{num}}~\OPT{\NT{hint-bases}}
 %%
-\nlsep \TERM{autotdb}~\OPT{\NT{int}}
-\nlsep \TERM{cdhyp}~\NT{ident}
-\nlsep \TERM{dhyp}~\NT{ident}
-\nlsep \TERM{dconcl}
-\nlsep \TERM{superauto}~\NT{auto-args}
-\nlsep \TERM{auto}~\OPT{\NT{int}}~\TERM{decomp}~\OPT{\NT{int}}
+%%\nlsep \TERM{autotdb}~\OPT{\NT{num}}
+%%\nlsep \TERM{cdhyp}~\NT{ident}
+%%\nlsep \TERM{dhyp}~\NT{ident}
+%%\nlsep \TERM{dconcl}
+%%\nlsep \TERM{superauto}~\NT{auto-args}
+\nlsep \TERM{auto}~\OPT{\NT{num}}~\TERM{decomp}~\OPT{\NT{num}}
 %%
 \nlsep \TERM{clear}~\PLUS{\NT{ident}}
 \nlsep \TERM{clearbody}~\PLUS{\NT{ident}}
@@ -457,7 +462,7 @@ $$
 \nlsep \TERM{right}~\OPT{\NT{with-binding-list}}
 \nlsep \TERM{split}~\OPT{\NT{with-binding-list}}
 \nlsep \TERM{exists}~\OPT{\NT{binding-list}}
-\nlsep \TERM{constructor}~\NT{int}~\OPT{\NT{with-binding-list}}
+\nlsep \TERM{constructor}~\NT{num}~\OPT{\NT{with-binding-list}}
 \nlsep \TERM{constructor}~\OPT{\NT{tactic}}
 %%
 \nlsep \TERM{reflexivity}
@@ -571,7 +576,7 @@ Conflicts exists between integers and constrs.
 \nlsep \KWD{with}~\PLUS{\NT{ident}}
 \SEPDEF
 \DEFNT{auto-args}
-       \OPT{\NT{int}}~\OPTGR{\TERM{adding}~\TERM{[}~\PLUS{\NT{reference}}
+       \OPT{\NT{num}}~\OPTGR{\TERM{adding}~\TERM{[}~\PLUS{\NT{reference}}
        ~\TERM{]}}~\OPT{\TERM{destructuring}}~\OPTGR{\TERM{using}~\TERM{tdb}}
 \end{rules}
 
@@ -610,7 +615,7 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \nlsep \TERM{first}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
 \nlsep \TERM{solve}~\TERM{[} ~\NT{tactic-seq} ~\TERM{]}
 \nlsep \TERM{idtac}
-\nlsep \TERM{fail} ~\OPT{\NT{int}} ~\OPT{\NT{string}}
+\nlsep \TERM{fail} ~\OPT{\NT{num}} ~\OPT{\NT{string}}
 \nlsep \TERM{constr}~\KWD{:}~\tacconstr
 \nlsep \NT{term-ltac}
 \nlsep \NT{reference}~\STAR{\NT{tactic-arg}}  &&\RNAME{call-tactic}
@@ -732,7 +737,7 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \nlsep \TERM{tauto}
 \nlsep \TERM{simplif}
 \nlsep \TERM{intuition}~\OPT{\NTL{tactic}{0}}
-\nlsep \TERM{linearintuition}~\OPT{\NT{int}}
+\nlsep \TERM{linearintuition}~\OPT{\NT{num}}
 %% contrib/cc
 \nlsep \TERM{cc}
 %% contrib/field
@@ -741,14 +746,14 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ?
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}}
 \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}}
-\nlsep \TERM{gtauto}
-\nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}}
+%%\nlsep \TERM{gtauto}
+%%\nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}}
 %% contrib/fourier
 \nlsep \TERM{fourierZ}
 %% contrib/funind
 \nlsep \TERM{functional}~\TERM{induction}~\tacconstr~\PLUS{\tacconstr}
 %% contrib/jprover
-\nlsep \TERM{jp}~\OPT{\NT{int}}
+\nlsep \TERM{jp}~\OPT{\NT{num}}
 %% contrib/omega
 \nlsep \TERM{omega}
 %% contrib/ring
@@ -786,7 +791,7 @@ $$
 \nlsep \NT{syntax}~\TERM{.}
 \nlsep \TERM{[}~\PLUS{\NT{vernac}}~\TERM{]}~\TERM{.}
 %%
-\nlsep \OPTGR{\NT{int}~\KWD{:}}~\NT{subgoal-command}~\TERM{.} ~~~&0
+\nlsep \OPTGR{\NT{num}~\KWD{:}}~\NT{subgoal-command}~\TERM{.} ~~~&0
 \SEPDEF
 \DEFNT{subgoal-command}
        \NT{check-command}
@@ -803,8 +808,8 @@ $$
 \nlsep \NT{assum-token}~\NT{assum-list}
 \nlsep \NT{finite-token}~\NT{inductive-definition}
       ~\STARGR{\KWD{with}~\NT{inductive-definition}}
-\nlsep \TERM{Fixpoint}~\NT{rec-definitions}
-\nlsep \TERM{CoFixpoint}~\NT{rec-definitions}
+\nlsep \TERM{Fixpoint}~\NT{fix-decl}~\STARGR{\KWD{with}~\NT{fix-decl}}
+\nlsep \TERM{CoFixpoint}~\NT{fix-decl}~\STARGR{\KWD{with}~\NT{fix-decl}}
 \nlsep \TERM{Scheme}~\NT{scheme}~\STARGR{\KWD{with}~\NT{scheme}}
 %% Extension: record
 \nlsep \NT{record-tok}~\OPT{\TERM{$>$}}~\NT{ident}~\STAR{\NT{binder-let}}
@@ -877,13 +882,6 @@ $$
 \SEPDEF
 \DEFNT{type-cstr-coe} \OPTGR{\NT{coerce-kwd}~\NT{constr}}
 \SEPDEF
-\DEFNT{rec-definitions}
-       \NT{rec-definition}~\STARGR{\KWD{with}~\NT{rec-definition}}
-\SEPDEF
-\DEFNT{rec-definition}
-       \NT{ident}~\STAR{\NT{binder-let}}~\OPT{\NT{annot}}~\NT{type-cstr}
-       ~\KWD{:=}~\NT{constr}
-\SEPDEF
 \DEFNT{scheme}
        \NT{ident}~\KWD{:=}~\NT{dep-scheme}~\KWD{for}~\NT{reference}
        ~\TERM{Sort}~\NT{sort}
@@ -954,7 +952,7 @@ $$
        ~\NT{class-rawexpr}~\TERM{$>->$}~\NT{class-rawexpr}
 \nlsep \TERM{Identity}~\TERM{Coercion}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:}
        ~\NT{class-rawexpr}~\TERM{$>->$}~\NT{class-rawexpr}
-\nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}~\TERM{[}~\STAR{\NT{int}}~\TERM{]}
+\nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}~\TERM{[}~\STAR{\NT{num}}~\TERM{]}
 \nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}
 \nlsep \TERM{Implicit}~\KWD{Type}~\PLUS{\NT{ident}}~\KWD{:}~\NT{constr}
 \SEPDEF
@@ -976,7 +974,7 @@ $$
 \nlsep \KWD{Type}~\NT{constr}
 \nlsep \TERM{Print}~\OPT{\NT{printable}}
 \nlsep \TERM{Print}~\NT{reference}
-\nlsep \TERM{Inspect}~\NT{int}
+\nlsep \TERM{Inspect}~\NT{num}
 \nlsep \TERM{About}~\NT{reference}
 %%
 \nlsep \TERM{Search}~\NT{reference}~\OPT{\NT{in-out-modules}}
@@ -1030,7 +1028,7 @@ $$
 \nlsep \TERM{Scopes}
 \nlsep \TERM{Scope}~\NT{ident}
 \nlsep \TERM{Visibility}~\OPT{\NT{ident}}
-\nlsep \TERM{Implicit}~\NT{qualid}
+\nlsep \TERM{Implicit}~\NT{reference}
 \SEPDEF
 \DEFNT{class-rawexpr}
        \TERM{Funclass}~\mid~\TERM{Sortclass}~\mid~\NT{reference}
@@ -1057,7 +1055,6 @@ $$
 \DEFNT{comment}
        \NT{constr}
 \nlsep \NT{string}
-\nlsep \NT{int}
 \end{rules}
 
 \subsection{Other commands}
@@ -1071,11 +1068,11 @@ $$
 \nlsep \TERM{Add}~\TERM{setoid}~\tacconstr~\tacconstr~\tacconstr
 \nlsep \TERM{Add}~\TERM{morphism}~\tacconstr~\KWD{:}~\NT{ident}
 \nlsep \TERM{Derive}~\TERM{inversion_clear}
-         ~\OPT{\NT{int}}~\NT{ident}~\NT{ident}
+         ~\OPT{\NT{num}}~\NT{ident}~\NT{ident}
 \nlsep \TERM{Derive}~\TERM{inversion_clear}
          ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
 \nlsep \TERM{Derive}~\TERM{inversion}
-         ~\OPT{\NT{int}}~\NT{ident}~\NT{ident}
+         ~\OPT{\NT{num}}~\NT{ident}~\NT{ident}
 \nlsep \TERM{Derive}~\TERM{inversion}
          ~\NT{ident}~\KWD{with}~\tacconstr~\OPTGR{\TERM{Sort}~\NT{sort}}
 \nlsep \TERM{Derive}~\TERM{dependent}~\TERM{inversion_clear}
@@ -1085,7 +1082,7 @@ $$
 %% Correctness: obsolete ?
 %\nlsep Correctness
 %\nlsep Global Variable
-%% extraction
+%% TODO: extraction
 \nlsep Extraction ...
 %% field
 \nlsep \TERM{Add}~\TERM{Field}~\tacconstr~\tacconstr~\tacconstr
@@ -1136,7 +1133,7 @@ $$
 \nlsep \TERM{Restore}~\TERM{State}~\NT{string}
 \nlsep \TERM{Reset}~\NT{ident}
 \nlsep \TERM{Reset}~\TERM{Initial}
-\nlsep \TERM{Back}~\OPT{\NT{int}}
+\nlsep \TERM{Back}~\OPT{\NT{num}}
 \end{rules}
 
 \subsection{Proof-editing commands}
@@ -1148,18 +1145,18 @@ $$
 \nlsep \TERM{Proof}~\KWD{with}~\NT{tactic}
 \nlsep \TERM{Abort}~\OPT{\TERM{All}}
 \nlsep \TERM{Abort}~\NT{ident}
-\nlsep \TERM{Existential}~\NT{int}~\NT{constr-body}
+\nlsep \TERM{Existential}~\NT{num}~\NT{constr-body}
 \nlsep \TERM{Qed}
 \nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\NT{ident}}
 \nlsep \TERM{Defined}~\OPT{\NT{ident}}
 \nlsep \TERM{Suspend}
 \nlsep \TERM{Resume}~\OPT{\NT{ident}}
 \nlsep \TERM{Restart}
-\nlsep \TERM{Undo}~\OPT{\NT{int}}
-\nlsep \TERM{Focus}~\OPT{\NT{int}}
+\nlsep \TERM{Undo}~\OPT{\NT{num}}
+\nlsep \TERM{Focus}~\OPT{\NT{num}}
 \nlsep \TERM{Unfocus}
-\nlsep \TERM{Show}~\OPT{\NT{int}}
-\nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{int}}
+\nlsep \TERM{Show}~\OPT{\NT{num}}
+\nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{num}}
 \nlsep \TERM{Show}~\TERM{Node}
 \nlsep \TERM{Show}~\TERM{Script}
 \nlsep \TERM{Show}~\TERM{Existentials}
@@ -1170,7 +1167,7 @@ $$
 \nlsep \TERM{Show}~\TERM{Intros}
 %% Correctness: obsolete ?
 %%\nlsep \TERM{Show}~\TERM{Programs}
-\nlsep \TERM{Explain}~\TERM{Proof}~\OPT{\TERM{Tree}}~\STAR{\NT{int}}
+\nlsep \TERM{Explain}~\TERM{Proof}~\OPT{\TERM{Tree}}~\STAR{\NT{num}}
 %% Go not documented
 \nlsep \TERM{Hint}~\OPT{\TERM{Local}}~\NT{hint}~\OPT{\NT{inbases}}
 %% PrintConstr not documented
@@ -1186,8 +1183,8 @@ $$
 \nlsep \TERM{Immediate}~\PLUS{\NTL{constr}{9}}
 \nlsep \TERM{Unfold}~\PLUS{\NT{reference}}
 \nlsep \TERM{Constructors}~\PLUS{\NT{reference}}
-\nlsep \TERM{Extern}~\NT{int}~\NT{constr}~\KWD{$\Rightarrow$}~\NT{tactic}
-\nlsep \TERM{Destruct}~\NT{ident}~\KWD{:=}~\NT{int}~\NT{destruct-loc}
+\nlsep \TERM{Extern}~\NT{num}~\NT{constr}~\KWD{$\Rightarrow$}~\NT{tactic}
+\nlsep \TERM{Destruct}~\NT{ident}~\KWD{:=}~\NT{num}~\NT{destruct-loc}
        ~\NT{constr}~\KWD{$\Rightarrow$}~\NT{tactic}
 \nlsep \TERM{Rewrite}~\NT{orient}~\PLUS{\NTL{constr}{9}}
        ~\OPTGR{\KWD{using}~\NT{tactic}}
@@ -1211,7 +1208,7 @@ $$
 \nlsep \TERM{Bind}~\TERM{Scope}~\NT{ident}~\KWD{with}~\PLUS{\NT{class-rawexpr}}
 \nlsep \TERM{Arguments}~\TERM{Scope}~\NT{reference}
        ~\TERM{[}~\PLUS{\NT{name}}~\TERM{]}
-\nlsep \TERM{Infix}~\OPT{\TERM{Local}} %%% ~\NT{prec}~\OPT{\NT{int}}
+\nlsep \TERM{Infix}~\OPT{\TERM{Local}} %%% ~\NT{prec}~\OPT{\NT{num}}
        ~\NT{string}~\KWD{:=}~\NT{reference}~\OPT{\NT{modifiers}}
        ~\OPT{\NT{in-scope}}
 \nlsep \TERM{Notation}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:=}~\NT{constr}
@@ -1227,9 +1224,9 @@ $$
 \nlsep \NT{modifier}~\KWD{,}~\NT{mod-list}
 \SEPDEF
 \DEFNT{modifier}
-       \NT{ident}~\KWD{at}~\NT{int}
-\nlsep \NT{ident}~\STARGR{\KWD{,}~\NT{ident}}~\KWD{at}~\NT{int}
-\nlsep \KWD{at}~\TERM{level}~\NT{int}
+       \NT{ident}~\KWD{at}~\NT{num}
+\nlsep \NT{ident}~\STARGR{\KWD{,}~\NT{ident}}~\KWD{at}~\NT{num}
+\nlsep \KWD{at}~\TERM{level}~\NT{num}
 \nlsep \TERM{left}~\TERM{associativity}
 \nlsep \TERM{right}~\TERM{associativity}
 \nlsep \TERM{no}~\TERM{associativity}
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index a39cfc4b5..c57e7761d 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -136,7 +136,7 @@ GEXTEND Gram
 	  ConstrMayEval (ConstrEval (rtc,c))
       | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
 	  ConstrMayEval (ConstrContext (id,c))
-      | IDENT "type"; "of"; c = Constr.constr ->
+      | IDENT "type"; IDENT "of"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
       | IDENT "fresh"; s = OPT STRING ->
 	  TacFreshId s ] ]
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 4975aed3c..24f2be581 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -134,7 +134,7 @@ GEXTEND Gram
     [ [ n = integer  -> Genarg.ArgArg n
       | id = identref -> Genarg.ArgVar id ] ]
   ;
-  autoarg_depth:
+(*  autoarg_depth:
   [ [ n = OPT natural -> n ] ]
   ;
   autoarg_adding:
@@ -144,12 +144,12 @@ GEXTEND Gram
   [ [ IDENT "destructing" -> true | -> false ] ]
   ;
   autoarg_usingTDB:
-  [ [ "using"; "tdb"  -> true | -> false ] ]
+  [ [ "using"; IDENT "tdb"  -> true | -> false ] ]
   ;
   autoargs:
   [ [ a0 = autoarg_depth; l = autoarg_adding; 
       a2 = autoarg_destructing; a3 = autoarg_usingTDB -> (a0,l,a2,a3) ] ]
-  ;
+  ;*)
   (* An identifier or a quotation meta-variable *)
   id_or_meta:
     [ [ id = identref -> AI id 
@@ -251,8 +251,10 @@ GEXTEND Gram
   ;
   hypident:
     [ [ id = id_or_meta -> id,(InHyp,ref None)
-      | "("; IDENT "type"; "of"; id = id_or_meta; ")" -> id,(InHypTypeOnly,ref None)
-      | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id,(InHypValueOnly,ref None)
+      | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
+          id,(InHypTypeOnly,ref None)
+      | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
+          id,(InHypValueOnly,ref None)
     ] ]
   ;
   hypident_occ:
@@ -371,11 +373,13 @@ GEXTEND Gram
       | IDENT "trivial"; db = hintbases -> TacTrivial db
       | IDENT "auto"; n = OPT natural; db = hintbases -> TacAuto (n, db)
 
+(* Obsolete since V8.0
       | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n
       | IDENT "cdhyp"; id = identref -> TacDestructHyp (true,id)
       | IDENT "dhyp";  id = identref -> TacDestructHyp (false,id)
       | IDENT "dconcl"  -> TacDestructConcl
       | IDENT "superauto"; l = autoargs -> TacSuperAuto l
+*)
       | IDENT "auto"; n = OPT natural; IDENT "decomp"; p = OPT natural ->
 	  TacDAuto (n, p)
 
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index eb41db74a..8c0b6ef73 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -110,7 +110,7 @@ GEXTEND Gram
 	  test_plurial_form l;
 	  VernacAssumption (stre, l)
       (* Gallina inductive declarations *)
-      | (* Non porté (?) : OPT[IDENT "Mutual"];*) f = finite_token;
+      | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
           VernacInductive (f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 01b210ac3..eff274988 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -94,7 +94,7 @@ type interp_sign =
 
 let check_is_value = function
   | VRTactic _ -> (* These are goals produced by Match *)
-   error "Immediate Match producing tactics not allowed in local definitions"
+   error "Immediate match producing tactics not allowed in local definitions"
   | _ -> ()
 
 (* For tactic_of_value *)
@@ -104,8 +104,7 @@ exception NotTactic
 let constr_of_VConstr_context = function
   | VConstr_context c -> c
   | _ ->
-    anomalylabstrm "constr_of_VConstr_context" (str
-      "Not a Constr_context tactic_arg")
+    errorlabstrm "constr_of_VConstr_context" (str "not a context variable")
 
 (* Displays a value *)
 let pr_value env = function
@@ -237,10 +236,17 @@ let coerce_to_inductive = function
 	errorlabstrm "coerce_to_inductive"
           (str "Found an argument which should be an inductive type")
 
+
+(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
+let initmactab = ref Gmap.empty
+
+
 (* Summary and Object declaration *)
 let mactab = ref Gmap.empty
 
-let lookup r = Gmap.find r !mactab
+let lookup r =
+  try Gmap.find r !mactab
+  with Not_found -> Gmap.find r !initmactab
 
 let _ =
   let init () = mactab := Gmap.empty in
@@ -2075,9 +2081,9 @@ let (inMD,outMD) =
 (* Adds a definition for tactics in the table *)
 let make_absolute_name (loc,id) =
   let kn = Lib.make_kn id in
-  if Gmap.mem kn !mactab then
+  if Gmap.mem kn !mactab or Gmap.mem kn !initmactab then
     user_err_loc (loc,"Tacinterp.add_tacdef",
-      str "There is already an Ltac Definition named " ++ pr_id id);
+      str "There is already an Ltac named " ++ pr_id id);
   kn
 
 let make_empty_glob_sign () =
@@ -2099,6 +2105,12 @@ let add_tacdef isrec tacl =
     (fun (id,_) -> Options.if_verbose msgnl (pr_id id ++ str " is defined"))
     rfun
 
+let add_primitive_tactic s tac =
+  let kn = Lib.make_kn (id_of_string s) in
+(*  Nametab.push_tactic (Until 0) sp kn) defs;*)
+  initmactab := Gmap.add kn tac !initmactab
+
+
 (***************************************************************************)
 (* Other entry points *)
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 71b377f43..1a80e9811 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -64,6 +64,7 @@ val get_debug : unit -> debug_info
 (* Adds a definition for tactics in the table *)
 val add_tacdef :
   bool -> (identifier Util.located * raw_tactic_expr) list -> unit
+val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
 (* Adds an interpretation function for extra generic arguments *)
 type glob_sign = {
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4919dddac..84bb17a5b 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -192,17 +192,18 @@ let lfo_wrap n gl=
 TACTIC EXTEND Tauto
 | [ "Tauto" ] -> [ tauto ]
 END
-
+(* Obsolete sinve V8.0
 TACTIC EXTEND TSimplif
 | [ "Simplif" ] -> [ simplif_gen ]
 END
-
+*)
 TACTIC EXTEND Intuition
 | [ "Intuition" ] -> [ intuition_gen default_intuition_tac ]
 | [ "Intuition" tactic(t) ] -> [ intuition_gen (snd t) ]
 END
-
+(* Obsolete since V8.0
 TACTIC EXTEND LinearIntuition
 | [ "LinearIntuition" ] -> [ lfo_wrap (-1)]
 | [ "LinearIntuition" integer(n)] -> [ lfo_wrap n]
 END
+*)
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index b37a190db..8dd636c29 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -433,13 +433,18 @@ let rec pr_atom0 env = function
   | TacAnyConstructor None -> str "constructor"
   | TacTrivial (Some []) -> str "trivial"
   | TacAuto (None,Some []) -> str "auto"
-  | TacAutoTDB None -> str "autotdb"
-  | TacDestructConcl -> str "dconcl"
+(*  | TacAutoTDB None -> str "autotdb"
+  | TacDestructConcl -> str "dconcl"*)
   | TacReflexivity -> str "reflexivity"
   | t -> str "(" ++ pr_atom1 env t ++ str ")"
 
   (* Main tactic printer *)
 and pr_atom1 env = function
+  | TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl
+  | TacSuperAuto _ | TacExtend (_,
+    ("GTauto"|"GIntuition"|"TSimplif"|
+     "LinearIntuition"),_) ->
+      errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0")
   | TacExtend (loc,s,l) ->
       pr_with_comments loc
         (pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l)
@@ -556,7 +561,7 @@ and pr_atom1 env = function
   | TacTrivial db -> hov 0 (str "trivial" ++ pr_hintbases db)
   | TacAuto (None,Some []) as x -> pr_atom0 env x
   | TacAuto (n,db) -> hov 0 (str "auto" ++ pr_opt int n ++ pr_hintbases db)
-  | TacAutoTDB None as x -> pr_atom0 env x
+(*  | TacAutoTDB None as x -> pr_atom0 env x
   | TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n)
   | TacDestructHyp (true,id) ->
       hov 0 (str "cdhyp" ++ spc () ++ pr_located pr_id id)
@@ -565,7 +570,7 @@ and pr_atom1 env = function
   | TacDestructConcl as x -> pr_atom0 env x
   | TacSuperAuto (n,l,b1,b2) ->
       hov 1 (str "superauto" ++ pr_opt int n ++ pr_autoarg_adding l ++ 
-             pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)
+             pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)*)
   | TacDAuto (n,p) ->
       hov 1 (str "auto" ++ pr_opt int n ++ str "decomp" ++ pr_opt int p)
 
@@ -653,7 +658,7 @@ let rec pr_tac env inherited tac =
       str "abstract " ++ pr_tac env (labstract,L) t, labstract
   | TacAbstract (t,Some s) -> 
       hov 0
-       (str "abstract " ++ pr_tac env (labstract,L) t ++ spc () ++
+       (str "abstract (" ++ pr_tac env (labstract,L) t ++ str")" ++ spc () ++
         str "using " ++ pr_id s),
       labstract
   | TacLetRecIn (l,t) ->