From 0ac79cca3c9f135df4138d1e43afc2b912766974 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 21 Nov 2017 16:36:10 +0100 Subject: Fix typo in doc optindex for Typeclass Resolution ... --- doc/refman/Classes.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 22c75b4fc8..d4d7fbd88e 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -519,14 +519,14 @@ potentially more expensive proof-search (i.e. more useless backtracking). \subsection{\tt Set Typeclass Resolution After Apply} -\optindex{Typeclasses Resolution After Apply} +\optindex{Typeclass Resolution After Apply} \emph{Deprecated since 8.6} This option (off by default in Coq 8.6 and 8.5) controls the resolution of typeclass subgoals generated by the {\tt apply} tactic. \subsection{\tt Set Typeclass Resolution For Conversion} -\optindex{Typeclasses Resolution For Conversion} +\optindex{Typeclass Resolution For Conversion} This option (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during -- cgit v1.2.3 From 9621d7af85f762a9b0266da5826510c4b4ffb6b2 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 21 Nov 2017 17:04:18 +0100 Subject: Add doc for Set Congruence Verbose --- doc/refman/RefMan-tac.tex | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 675c2bf174..f29dfa30b4 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4710,6 +4710,13 @@ congruence. described above. \end{ErrMsgs} +\noindent {\bf Remark: } {\tt congruence} can be made to print debug +information by setting the following option: + +\begin{quote} +\optindex{Congruence Verbose} +{\tt Set Congruence Verbose} +\end{quote} \section{Checking properties of terms} -- cgit v1.2.3 From 60f6795213b7e2e3fd0f5e9d63558ce1aae346b8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 21 Nov 2017 17:04:35 +0100 Subject: Add optindex for Set Bullet Behavior. --- doc/refman/RefMan-pro.tex | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 8f659ded35..1d3311edc2 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -395,6 +395,8 @@ Proof. \end{ErrMsgs} +\subsection[\tt Set Bullet Behavior.]{\tt Set Bullet Behavior.\optindex{Bullet Behavior}} + The bullet behavior can be controlled by the following commands. \begin{quote} -- cgit v1.2.3 From 91aa16b412225049e9cb360d8e06c0200e29afc1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 21 Nov 2017 17:04:50 +0100 Subject: Add doc for Set Info/Debug Auto/Trivial/Eauto. --- doc/refman/RefMan-tac.tex | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index f29dfa30b4..9833448015 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3703,6 +3703,9 @@ hints of the database named {\tt core}. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used. +\item {\tt debug auto} Behaves like {\tt auto} but shows the tactics + it tries to solve the goal, including failing paths. + \item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} \ident$_1$ {\ldots} \ident$_n$} @@ -3723,6 +3726,8 @@ hints of the database named {\tt core}. \item {\tt info\_trivial} +\item {\tt debug trivial} + \item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} \ident$_1$ {\ldots} \ident$_n$} @@ -3732,6 +3737,19 @@ hints of the database named {\tt core}. \Rem {\tt auto} either solves completely the goal or else leaves it intact. \texttt{auto} and \texttt{trivial} never fail. +\Rem The following options enable printing of informative or debug +information for the {\tt auto} and {\tt trivial} tactics: +\begin{quote} + \optindex{Info Auto} + {\tt Set Info Auto} + \optindex{Debug Auto} + {\tt Set Debug Auto} + \optindex{Info Trivial} + {\tt Set Info Trivial} + \optindex{Debug Trivial} + {\tt Set Debug Trivial} +\end{quote} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt eauto} @@ -3768,6 +3786,14 @@ Note that {\tt ex\_intro} should be declared as a hint. \end{Variants} +\Rem {\tt eauto} obeys the following options: +\begin{quote} + \optindex{Info Eauto} + {\tt Set Info Eauto} + \optindex{Debug Eauto} + {\tt Set Debug Eauto} +\end{quote} + \SeeAlso Section~\ref{Hints-databases} \subsection{\tt autounfold with \ident$_1$ \mbox{\dots} \ident$_n$} -- cgit v1.2.3 From 9eac0be2eb0ac450393172fa99d092da226a694b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 21 Nov 2017 17:10:16 +0100 Subject: Add doc for Set Debug Cbv. --- doc/refman/RefMan-tac.tex | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 9833448015..9307f5ced7 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3334,6 +3334,14 @@ evaluating purely computational expressions (i.e. with little dead code). \end{Variants} +\Rem The following option makes {\tt cbv} (and its derivative {\tt + compute}) print information about the constants it encounters and +the unfolding decisions it makes. +\begin{quote} + \optindex{Debug Cbv} + {\tt Set Debug Cbv} +\end{quote} + % Obsolete? Anyway not very important message %\begin{ErrMsgs} %\item \errindex{Delta must be specified before} -- cgit v1.2.3 From 125989fc2e9e0efa97dfc4ad3d41502e5d93ca56 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 21 Nov 2017 17:16:21 +0100 Subject: Add doc for Set Debug RAKAM. --- doc/refman/RefMan-tac.tex | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 9307f5ced7..66a5f107a5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3515,6 +3515,13 @@ of {\tt cbn} while doing reductions in unification, type inference and tactic applications. It can result in expensive unifications, as refolding currently uses a potentially exponential heuristic. +\begin{quote} + \optindex{Debug RAKAM} + {\tt Set Debug RAKAM} +\end{quote} +This option makes {\tt cbn} print various debugging information. +{\tt RAKAM} is the Refolding Algebraic Krivine Abstract Machine. + \subsection{\tt unfold \qualid} \tacindex{unfold} \label{unfold} -- cgit v1.2.3 From d6bd80ff477f3416f4ff0ded65aa658999b5ac21 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 24 Nov 2017 22:27:53 +0100 Subject: Document some omega options (missing Omega Oldstyle). --- doc/refman/Omega.tex | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex index 8025fbe29f..82765da6ed 100644 --- a/doc/refman/Omega.tex +++ b/doc/refman/Omega.tex @@ -149,6 +149,32 @@ intro; omega. % Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. +\section{Options} + +\begin{quote} + \optindex{Stable Omega} + {\tt Unset Stable Omega} +\end{quote} +This deprecated option (on by default) is for compatibility with Coq +pre 8.5. It resets internal name counters to make executions of +{\tt omega} independent. + +\begin{quote} + \optindex{Omega UseLocalDefs} + {\tt Unset Omega UseLocalDefs} +\end{quote} +This option (on by default) allows {\tt omega} to use the bodies of +local variables. + +\begin{quote} + \optindex{Omega System} + {\tt Set Omega System} + \optindex{Omega Action} + {\tt Set Omega Action} +\end{quote} +These two options (off by default) activate the printing of debug +information. + \asection{Technical data} \label{technical} -- cgit v1.2.3 From 0bca8c15643e7b5b894b822db4f50bfbbd0858bb Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 24 Nov 2017 22:48:05 +0100 Subject: Document Asymmetric Patterns. --- doc/refman/Cases.tex | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index 7ad895f9d8..376ef031db 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -280,6 +280,18 @@ Fail Check end). \end{coq_example} +The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns} +(off by default) removes parameters from constructors in patterns: +\begin{coq_example} + Set Asymmetric Patterns. + Check (fun l:List nat => + match l with + | nil => nil + | cons _ l' => l' + end) + Unset Asymmetric Patterns. +\end{coq_example} + \paragraph{Implicit arguments in patterns} By default, implicit arguments are omitted in patterns. So we write: -- cgit v1.2.3 From c43e06c343e2157b839dab8d62fb8345d3238c3c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 24 Nov 2017 23:22:18 +0100 Subject: Document Record Elimination Schemes. --- doc/refman/RefMan-sch.tex | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 956f308512..45460bc37a 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -127,6 +127,7 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Boolean Equality Schemes} \optindex{Elimination Schemes} \optindex{Nonrecursive Elimination Schemes} +\optindex{Record Elimination Schemes} \optindex{Case Analysis Schemes} \optindex{Decidable Equality Schemes} \label{set-nonrecursive-elimination-schemes} @@ -142,6 +143,7 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic declaration of the induction principles. It can be activated with the command {\tt Set Nonrecursive Elimination Schemes}. It can be deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. +{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}. In addition, the {\tt Case Analysis Schemes} flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the -- cgit v1.2.3 From e0ed58e702ea89db0d397d66ce0e223ac8ff50a8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 24 Nov 2017 23:27:52 +0100 Subject: Document Rewriting Schemes (quickly). --- doc/refman/RefMan-sch.tex | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 45460bc37a..30724759d2 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -130,6 +130,7 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Record Elimination Schemes} \optindex{Case Analysis Schemes} \optindex{Decidable Equality Schemes} +\optindex{Rewriting Schemes} \label{set-nonrecursive-elimination-schemes} } @@ -158,6 +159,9 @@ However you have to be careful with this option since \Coq~ may now reject well-defined inductive types because it cannot compute a Boolean equality for them. +The {\tt Rewriting Schemes} flag governs generation of equality +related schemes such as congruence. + \subsection{\tt Combined Scheme} \label{CombinedScheme} \comindex{Combined Scheme} -- cgit v1.2.3 From f9b715c4ea07d6ecfece7f28e4d25f3dcab01158 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 24 Nov 2017 23:58:36 +0100 Subject: Document Short Module Printing. --- doc/refman/RefMan-mod.tex | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index e56c8fa7fe..b4e270e6c3 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -403,10 +403,14 @@ Fail Check B.T. \end{Warnings} \subsection{\tt Print Module {\ident} -\comindex{Print Module}} +\comindex{Print Module} \optindex{Short Module Printing}} Prints the module type and (optionally) the body of the module {\ident}. +For this command and {\tt Print Module Type}, the option {\tt Short + Module Printing} (off by default) disables the printing of the types of fields, +leaving only their names. + \subsection{\tt Print Module Type {\ident} \comindex{Print Module Type}} -- cgit v1.2.3 From 30746e6a9a3296c1aacb2fc03e1c16014232219f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 21 Nov 2017 16:42:42 +0100 Subject: Deprecate dead code option Congruence Depth. --- plugins/firstorder/g_ground.ml4 | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 938bec25b9..b81010c7bd 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -40,17 +40,17 @@ let _= in declare_int_option gdopt -let congruence_depth=ref 100 let _= + let congruence_depth=ref 100 in let gdopt= - { optdepr=false; + { optdepr=true; (* noop *) optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); optwrite= (function - None->congruence_depth:=0 + None->congruence_depth:=0 | Some i->congruence_depth:=(max i 0))} in declare_int_option gdopt -- cgit v1.2.3 From 539a62a79f75f9f5190b9bd8edfbb04b880a5f1f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 24 Nov 2017 21:54:48 +0100 Subject: Deprecate dead option Match Strict (ssr). --- plugins/ssr/ssrequality.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index bd9633afbd..6032ed2af8 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -143,14 +143,14 @@ let newssrcongrtac arg ist gl = (** Coq rewrite compatibility flag *) -let ssr_strict_match = ref false let _ = - Goptions.declare_bool_option + let ssr_strict_match = ref false in + Goptions.declare_bool_option { Goptions.optname = "strict redex matching"; Goptions.optkey = ["Match"; "Strict"]; Goptions.optread = (fun () -> !ssr_strict_match); - Goptions.optdepr = false; + Goptions.optdepr = true; (* noop *) Goptions.optwrite = (fun b -> ssr_strict_match := b) } (** Rewrite rules *) -- cgit v1.2.3