From b946944cb9bb21dcd9aba3b01b9aeafc4b78b1c8 Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 23 Dec 2003 18:18:13 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5134 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 4 +- contrib/first-order/g_ground.ml4 | 3 +- doc/syntax-v8.tex | 121 +++++++++++++++++++-------------------- parsing/g_ltacnew.ml4 | 2 +- parsing/g_tacticnew.ml4 | 14 +++-- parsing/g_vernacnew.ml4 | 2 +- tactics/tacinterp.ml | 24 ++++++-- tactics/tacinterp.mli | 1 + tactics/tauto.ml4 | 7 ++- translate/pptacticnew.ml | 15 +++-- 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) -> -- cgit v1.2.3