aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES4
-rw-r--r--contrib/first-order/g_ground.ml43
-rw-r--r--doc/syntax-v8.tex121
-rw-r--r--parsing/g_ltacnew.ml42
-rw-r--r--parsing/g_tacticnew.ml414
-rw-r--r--parsing/g_vernacnew.ml42
-rw-r--r--tactics/tacinterp.ml24
-rw-r--r--tactics/tacinterp.mli1
-rw-r--r--tactics/tauto.ml47
-rw-r--r--translate/pptacticnew.ml15
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) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 13:57:47 +0000