diff options
| author | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
| commit | 4bb062f4a66c4ae5a1742e7d99fdc335de0d57a9 (patch) | |
| tree | af8ead1cdc5af3842e683f602177ab4fa2dec9b5 | |
| parent | 1be9c4da4d814c29d4ba45b121fda924adc1130e (diff) | |
| parent | 29ba692f0fd25ce87392bbb7494cb62e3b97dc07 (diff) | |
Merge branch 'v8.5'
62 files changed, 423 insertions, 538 deletions
@@ -62,9 +62,6 @@ Vernacular commands Coq: terms, modules, tactics, etc. The old behavior of the command can be retrieved using the "Locate Term" command. - New "Derive" command to help writing program by derivation. -- "Undo" undoes any command, not just tactics. -- "Undo. Undo." does not work in CoqIDE or Proof General, it works only - in coqtop. "Undo 2" should be used intead. - New "Refine Instance Mode" option that allows to deactivate the generation of obligations in incomplete typeclass instances, raising an error instead. - "Collection" command to name sets of section hypotheses. Named collections diff --git a/Makefile.doc b/Makefile.doc index 33dd60dbad..1f35093510 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -99,6 +99,8 @@ doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(MAKEINDEX) -q Reference-Manual.comidx -o Reference-Manual.comind;\ $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ + $(MAKEINDEX) -q Reference-Manual.optidx -o Reference-Manual.optind;\ + $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(MAKEINDEX) -q Reference-Manual.erridx -o Reference-Manual.errind;\ $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ @@ -24,8 +24,6 @@ ## tags for camlp4 files -"toplevel/whelp.ml4": use_grammar - "parsing/g_constr.ml4": use_compat5 "parsing/g_ltac.ml4": use_compat5 "parsing/g_prim.ml4": use_compat5 @@ -74,4 +72,4 @@ "tools/coqdoc": include "toplevel": include -<plugins/**>: include
\ No newline at end of file +<plugins/**>: include diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index 7b8f829601..db82717094 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -88,6 +88,7 @@ <ul class="menu"> <li><a href="general-index.html">General</a></li> <li><a href="command-index.html">Commands</a></li> + <li><a href="option-index.html">Options</a></li> <li><a href="tactic-index.html">Tactics</a></li> <li><a href="error-index.html">Errors</a></li> </ul> diff --git a/doc/common/styles/html/coqremote/styles.hva b/doc/common/styles/html/coqremote/styles.hva index 94fb0d38b1..a09dc4f85f 100644 --- a/doc/common/styles/html/coqremote/styles.hva +++ b/doc/common/styles/html/coqremote/styles.hva @@ -53,6 +53,7 @@ <ul class="menu"> <li><a href="general-index.html">General</a></li> <li><a href="command-index.html">Commands</a></li> + <li><a href="option-index.html">Options</a></li> <li><a href="tactic-index.html">Tactics</a></li> <li><a href="error-index.html">Errors</a></li> </ul> diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html index c2ac2c19d8..1641a1ed37 100644 --- a/doc/common/styles/html/simple/cover.html +++ b/doc/common/styles/html/simple/cover.html @@ -58,6 +58,7 @@ <li><a href="toc.html">Table of contents</a></li> <li><a href="general-index.html">General index</a></li> <li><a href="command-index.html">Commands index</a></li> + <li><a href="option-index.html">Options index</a></li> <li><a href="tactic-index.html">Tactics index</a></li> <li><a href="error-index.html">Errors index</a></li> </ul> diff --git a/doc/common/styles/html/simple/styles.hva b/doc/common/styles/html/simple/styles.hva index 71c4ffedf0..20d0d4dd0a 100644 --- a/doc/common/styles/html/simple/styles.hva +++ b/doc/common/styles/html/simple/styles.hva @@ -32,6 +32,7 @@ <li><a href="toc.html">Table of contents</a></li> <li><a href="general-index.html">General index</a></li> <li><a href="command-index.html">Commands index</a></li> + <li><a href="option-index.html">Options index</a></li> <li><a href="tactic-index.html">Tactics index</a></li> <li><a href="error-index.html">Errors index</a></li> </ul> diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 35d64053c1..96b486cdfa 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -414,7 +414,7 @@ based on a variant of eauto. The flags semantics are: \end{itemize} \subsection{\tt Set Refine Instance Mode} -\comindex{Set Refine Instance Mode}\comindex{Unset Refine Instance Mode} +\optindex{Refine Instance Mode} The option {\tt Refine Instance Mode} allows to switch the behavior of instance declarations made through the {\tt Instance} command. diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex index 60b4b22411..e4aa69353d 100644 --- a/doc/refman/Coercion.tex +++ b/doc/refman/Coercion.tex @@ -305,8 +305,7 @@ Print the list of valid coercion paths from {\class$_1$} to {\class$_2$}. \asection{Activating the Printing of Coercions} \asubsection{\tt Set Printing Coercions.} -\comindex{Set Printing Coercions} -\comindex{Unset Printing Coercions} +\optindex{Printing Coercions} This command forces all the coercions to be printed. Conversely, to skip the printing of coercions, use @@ -314,8 +313,7 @@ Conversely, to skip the printing of coercions, use By default, coercions are not printed. \asubsection{\tt Set Printing Coercion {\qualid}.} -\comindex{Set Printing Coercion} -\comindex{Unset Printing Coercion} +\optindex{Printing Coercion} This command forces coercion denoted by {\qualid} to be printed. To skip the printing of coercion {\qualid}, use @@ -378,8 +376,7 @@ imported or not. To recover the behavior of the versions of Coq prior to 8.3, use the following command: -\comindex{Set Automatic Coercions Import} -\comindex{Unset Automatic Coercions Import} +\optindex{Automatic Coercions Import} \begin{verbatim} Set Automatic Coercions Import. \end{verbatim} diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index e9664f791c..187fe53428 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -117,22 +117,20 @@ The type-preserving optimizations are controlled by the following \Coq\ options: \begin{description} -\item \comindex{Set Extraction Optimize} +\item \optindex{Extraction Optimize} {\tt Set Extraction Optimize.} -\item \comindex{Unset Extraction Optimize} -{\tt Unset Extraction Optimize.} +\item {\tt Unset Extraction Optimize.} Default is Set. This controls all type-preserving optimizations made on the ML terms (mostly reduction of dummy beta/iota redexes, but also simplifications on Cases, etc). Put this option to Unset if you want a ML term as close as possible to the Coq term. -\item \comindex{Set Extraction Conservative Types} +\item \optindex{Extraction Conservative Types} {\tt Set Extraction Conservative Types.} -\item \comindex{Unset Extraction Conservative Types} -{\tt Unset Extraction Conservative Types.} +\item {\tt Unset Extraction Conservative Types.} Default is Unset. This controls the non type-preserving optimizations made on ML terms (which try to avoid function abstraction of dummy @@ -140,11 +138,10 @@ types). Turn this option to Set to make sure that {\tt e:t} implies that {\tt e':t'} where {\tt e'} and {\tt t'} are the extracted code of {\tt e} and {\tt t} respectively. -\item \comindex{Set Extraction KeepSingleton} +\item \optindex{Extraction KeepSingleton} {\tt Set Extraction KeepSingleton.} -\item \comindex{Unset Extraction KeepSingleton} -{\tt Unset Extraction KeepSingleton.} +\item {\tt Unset Extraction KeepSingleton.} Default is Unset. Normally, when the extraction of an inductive type produces a singleton type (i.e. a type with only one constructor, and @@ -153,11 +150,10 @@ removed and this type is seen as an alias to the inner type. The typical example is {\tt sig}. This option allows disabling this optimization when one wishes to preserve the inductive structure of types. -\item \comindex{Set Extraction AutoInline} +\item \optindex{Extraction AutoInline} {\tt Set Extraction AutoInline.} -\item \comindex{Unset Extraction AutoInline} -{\tt Unset Extraction AutoInline.} +\item {\tt Unset Extraction AutoInline.} Default is Set, so by default, the extraction mechanism is free to inline the bodies of some defined constants, according to some heuristics diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 193c9d16a3..e802398b55 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -253,14 +253,14 @@ tactic is replaced by the default one if not specified. \item {\tt Preterm [of \ident]}\comindex{Preterm} Shows the term that will be fed to the kernel once the obligations are solved. Useful for debugging. -\item {\tt Set Transparent Obligations}\comindex{Set Transparent Obligations} +\item {\tt Set Transparent Obligations}\optindex{Transparent Obligations} Control whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque. -\item {\tt Set Hide Obligations}\comindex{Set Hide Obligations} +\item {\tt Set Hide Obligations}\optindex{Hide Obligations} Control whether obligations appearing in the term should be hidden as implicit arguments of the special constant \texttt{Program.Tactics.obligation}. -\item {\tt Set Shrink Obligations}\comindex{Set Shrink Obligations} +\item {\tt Set Shrink Obligations}\optindex{Shrink Obligations} Control whether obligations defined by tactics should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 11b4f26145..d1ce3bf41d 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -470,9 +470,7 @@ The following commands give some control over the pretty-printing of \subsubsection{Printing nested patterns \label{SetPrintingMatching} -\comindex{Set Printing Matching} -\comindex{Unset Printing Matching} -\comindex{Test Printing Matching}} +\optindex{Printing Matching}} The Calculus of Inductive Constructions knows pattern-matching only over simple patterns. It is however convenient to re-factorize nested @@ -498,9 +496,7 @@ This tells if the printing matching mode is on or off. The default is on. \subsubsection{Printing of wildcard pattern -\comindex{Set Printing Wildcard} -\comindex{Unset Printing Wildcard} -\comindex{Test Printing Wildcard}} +\optindex{Printing Wildcard}} Some variables in a pattern may not occur in the right-hand side of the pattern-matching clause. There are options to control the @@ -527,9 +523,7 @@ This tells if the wildcard printing mode is on or off. The default is to print wildcard for useless variables. \subsubsection{Printing of the elimination predicate -\comindex{Set Printing Synth} -\comindex{Unset Printing Synth} -\comindex{Test Printing Synth}} +\optindex{Printing Synth}} In most of the cases, the type of the result of a matched term is mechanically synthesizable. Especially, if the result type does not @@ -1451,8 +1445,7 @@ Check (p r1 r2). \subsection{Mode for automatic declaration of implicit arguments \label{Auto-implicit} -\comindex{Set Implicit Arguments} -\comindex{Unset Implicit Arguments}} +\optindex{Implicit Arguments}} In case one wants to systematically declare implicit the arguments detectable as such, one may switch to the automatic declaration of @@ -1466,8 +1459,7 @@ arguments is governed by options controlling whether strict and contextual implicit arguments have to be considered or not. \subsection{Controlling strict implicit arguments -\comindex{Set Strict Implicit} -\comindex{Unset Strict Implicit} +\optindex{Strict Implicit} \label{SetStrictImplicit}} When the mode for automatic declaration of implicit arguments is on, @@ -1482,8 +1474,7 @@ Conversely, use the command {\tt Set Strict Implicit} to restore the original mode that declares implicit only the strict implicit arguments plus a small subset of the non strict implicit arguments. In the other way round, to capture exactly the strict implicit arguments and no more than the strict implicit arguments, use the command: -\comindex{Set Strongly Strict Implicit} -\comindex{Unset Strongly Strict Implicit} +\optindex{Strongly Strict Implicit} \begin{quote} \tt Set Strongly Strict Implicit. \end{quote} @@ -1494,8 +1485,7 @@ let the option ``{\tt Strict Implicit}'' decide what to do. declare the strict implicit arguments as implicit. \subsection{Controlling contextual implicit arguments -\comindex{Set Contextual Implicit} -\comindex{Unset Contextual Implicit} +\optindex{Contextual Implicit} \label{SetContextualImplicit}} By default, {\Coq} does not automatically set implicit the contextual @@ -1508,8 +1498,7 @@ Conversely, use command {\tt Unset Contextual Implicit} to unset the contextual implicit mode. \subsection{Controlling reversible-pattern implicit arguments -\comindex{Set Reversible Pattern Implicit} -\comindex{Unset Reversible Pattern Implicit} +\optindex{Reversible Pattern Implicit} \label{SetReversiblePatternImplicit}} By default, {\Coq} does not automatically set implicit the reversible-pattern @@ -1522,8 +1511,7 @@ Conversely, use command {\tt Unset Reversible Pattern Implicit} to unset the reversible-pattern implicit mode. \subsection{Controlling the insertion of implicit arguments not followed by explicit arguments -\comindex{Set Maximal Implicit Insertion} -\comindex{Unset Maximal Implicit Insertion} +\optindex{Maximal Implicit Insertion} \label{SetMaximalImplicitInsertion}} Implicit arguments can be declared to be automatically inserted when a @@ -1607,10 +1595,8 @@ if each of them is to be used maximally or not, use the command \end{quote} \subsection{Explicit displaying of implicit arguments for pretty-printing -\comindex{Set Printing Implicit} -\comindex{Unset Printing Implicit} -\comindex{Set Printing Implicit Defensive} -\comindex{Unset Printing Implicit Defensive}} +\optindex{Printing Implicit} +\optindex{Printing Implicit Defensive}} By default the basic pretty-printing rules hide the inferable implicit arguments of an application. To force printing all implicit arguments, @@ -1653,8 +1639,7 @@ Check Prop = nat. \end{coq_example*} \subsection{Deactivation of implicit arguments for parsing} -\comindex{Set Parsing Explicit} -\comindex{Unset Parsing Explicit} +\optindex{Parsing Explicit} Use of implicit arguments can be deactivated by issuing the command: \begin{quote} @@ -1874,8 +1859,7 @@ More details and examples, and a description of the commands related to coercions are provided in Chapter~\ref{Coercions-full}. \section[Printing constructions in full]{Printing constructions in full\label{SetPrintingAll} -\comindex{Set Printing All} -\comindex{Unset Printing All}} +\optindex{Printing All}} Coercions, implicit arguments, the type of pattern-matching, but also notations (see Chapter~\ref{Addoc-syntax}) can obfuscate the behavior @@ -1897,8 +1881,7 @@ printing features, use the command \end{quote} \section[Printing universes]{Printing universes\label{PrintingUniverses} -\comindex{Set Printing Universes} -\comindex{Unset Printing Universes}} +\optindex{Printing Universes}} The following command: \begin{quote} @@ -1991,8 +1974,7 @@ Unset Printing Existential Instances. \subsection{Explicit displaying of existential instances for pretty-printing \label{SetPrintingExistentialInstances} -\comindex{Set Printing Existential Instances} -\comindex{Unset Printing Existential Instances}} +\optindex{Printing Existential Instances}} The command: \begin{quote} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 1704b4d60b..eea53886b8 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -779,8 +779,7 @@ f (3+4). \end{coq_example} \item \index{appcontext@\texttt{appcontext}!in pattern} - \comindex{Set Tactic Compat Context} - \comindex{Unset Tactic Compat Context} + \optindex{Tactic Compat Context} For historical reasons, {\tt context} used to consider $n$-ary applications such as {\tt (f 1 2)} as a whole, and not as a sequence of unary applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} would fail @@ -1094,9 +1093,7 @@ Defined {\ltac} functions can be displayed using the command \section{Debugging {\ltac} tactics} -\subsection[Info trace]{Info trace\comindex{Info}\comindex{Set Info Level} -\comindex{Unset Info Level} -\comindex{Test Info Level}} +\subsection[Info trace]{Info trace\comindex{Info}\optindex{Info Level}} It is possible to print the trace of the path eventually taken by an {\ltac} script. That is, the list of executed tactics, discarding all the branches which have failed. To that end the {\tt Info} command can be used with the following syntax. @@ -1142,9 +1139,7 @@ This will automatically print the same trace as {\tt Info \num} at each tactic c The current value for the {\tt Info Level} option can be checked using the {\tt Test Info Level} command. -\subsection[Interactive debugger]{Interactive debugger\comindex{Set Ltac Debug} -\comindex{Unset Ltac Debug} -\comindex{Test Ltac Debug}} +\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}} The {\ltac} interpreter comes with a step-by-step debugger. The debugger can be activated using the command diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 40e0ecc11c..32f94abf7a 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -101,6 +101,7 @@ This command sets {\rm\sl option} to {\rm\sl value}. The original value of \begin{Variants} \item {\tt Local Set {\rm\sl option} {\rm\sl value}.\comindex{Local Set}} This command sets {\rm\sl option} to {\rm\sl value}. The original value of +{\rm\sl option} is restored at the end of the module. \item {\tt Global Set {\rm\sl option} {\rm\sl value}.\comindex{Global Set}} This command sets {\rm\sl option} to {\rm\sl value}. The original value of {\rm\sl option} is \emph{not} restored at the end of the module. Additionally, @@ -489,90 +490,6 @@ Locate I.Dont.Exist. \SeeAlso Section \ref{LocateSymbol} -\subsection{The {\sc Whelp} searching tool -\label{Whelp}} - -{\sc Whelp} is an experimental searching and browsing tool for the -whole {\Coq} library and the whole set of {\Coq} user contributions. -{\sc Whelp} requires a browser to work. {\sc Whelp} has been developed -at the University of Bologna as part of the HELM\footnote{Hypertextual -Electronic Library of Mathematics} and MoWGLI\footnote{Mathematics on -the Web, Get it by Logics and Interfaces} projects. It can be invoked -directly from the {\Coq} toplevel or from {\CoqIDE}, assuming a -graphical environment is also running. The browser to use can be -selected by setting the environment variable {\tt -COQREMOTEBROWSER}. If not explicitly set, it defaults to -\verb!firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"! or -\verb!C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s!, depending on the -underlying operating system (in the command, the string \verb!%s! -serves as metavariable for the url to open). -The Whelp tool relies on a dedicated Whelp server and on another server -called Getter that retrieves formal documents. The default Whelp server name -can be obtained using the command {\tt Test Whelp Server} -\comindex{Test Whelp Server} and the default Getter can be obtained -using the command: {\tt Test Whelp Getter} \comindex{Test Whelp -Getter}. The Whelp server name can be changed using the command: - -\smallskip -\noindent {\tt Set Whelp Server {\str}}.\\ -where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58080}). -\comindex{Set Whelp Server} -\smallskip - -\noindent The Getter can be changed using the command: -\smallskip - -\noindent {\tt Set Whelp Getter {\str}}.\\ -where {\str} is a URL (e.g. {\tt http://mowgli.cs.unibo.it:58081}). -\comindex{Set Whelp Getter} - -\bigskip - -The {\sc Whelp} commands are: - -\subsubsection{\tt Whelp Locate "{\sl reg\_expr}". -\comindex{Whelp Locate}} - -This command opens a browser window and displays the result of seeking -for all names that match the regular expression {\sl reg\_expr} in the -{\Coq} library and user contributions. The regular expression can -contain the special operators are * and ? that respectively stand for -an arbitrary substring and for exactly one character. - -\variant {\tt Whelp Locate {\ident}.}\\ -This is equivalent to {\tt Whelp Locate "{\ident}"}. - -\subsubsection{\tt Whelp Match {\pattern}. -\comindex{Whelp Match}} - -This command opens a browser window and displays the result of seeking -for all statements that match the pattern {\pattern}. Holes in the -pattern are represented by the wildcard character ``\_''. - -\subsubsection[\tt Whelp Instance {\pattern}.]{\tt Whelp Instance {\pattern}.\comindex{Whelp Instance}} - -This command opens a browser window and displays the result of seeking -for all statements that are instances of the pattern {\pattern}. The -pattern is here assumed to be an universally quantified expression. - -\subsubsection[\tt Whelp Elim {\qualid}.]{\tt Whelp Elim {\qualid}.\comindex{Whelp Elim}} - -This command opens a browser window and displays the result of seeking -for all statements that have the ``form'' of an elimination scheme -over the type denoted by {\qualid}. - -\subsubsection[\tt Whelp Hint {\term}.]{\tt Whelp Hint {\term}.\comindex{Whelp Hint}} - -This command opens a browser window and displays the result of seeking -for all statements that can be instantiated so that to prove the -statement {\term}. - -\variant {\tt Whelp Hint.}\\ This is equivalent to {\tt Whelp Hint -{\sl goal}} where {\sl goal} is the current goal to prove. Notice that -{\Coq} does not send the local environment of definitions to the {\sc -Whelp} tool so that it only works on requests strictly based on, only, -definitions of the standard library and user contributions. - \section{Loading files} \Coq\ offers the possibility of loading different @@ -959,53 +876,53 @@ the command has not terminated after the time specified by the integer is displayed. \subsection[\tt Set Default Timeout \textrm{\textsl{int}}.]{\tt Set - Default Timeout \textrm{\textsl{int}}.\comindex{Set Default Timeout}} + Default Timeout \textrm{\textsl{int}}.\optindex{Default Timeout}} After using this command, all subsequent commands behave as if they were passed to a {\tt Timeout} command. Commands already starting by a {\tt Timeout} are unaffected. -\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\comindex{Unset Default Timeout}} +\subsection[\tt Unset Default Timeout.]{\tt Unset Default Timeout.\optindex{Default Timeout}} This command turns off the use of a default timeout. -\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\comindex{Test Default Timeout}} +\subsection[\tt Test Default Timeout.]{\tt Test Default Timeout.\optindex{Default Timeout}} This command displays whether some default timeout has be set or not. \section{Controlling display} -\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent} +\subsection[\tt Set Silent.]{\tt Set Silent.\optindex{Silent} \label{Begin-Silent} \index{Silent mode}} This command turns off the normal displaying. -\subsection[\tt Unset Silent.]{\tt Unset Silent.\comindex{Unset Silent}} +\subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}} This command turns the normal display on. -\subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\comindex{Set Printing Width}} +\subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\optindex{Printing Width}} \label{SetPrintingWidth} This command sets which left-aligned part of the width of the screen is used for display. -\subsection[\tt Unset Printing Width.]{\tt Unset Printing Width.\comindex{Unset Printing Width}} +\subsection[\tt Unset Printing Width.]{\tt Unset Printing Width.\optindex{Printing Width}} This command resets the width of the screen used for display to its default value (which is 78 at the time of writing this documentation). -\subsection[\tt Test Printing Width.]{\tt Test Printing Width.\comindex{Test Printing Width}} +\subsection[\tt Test Printing Width.]{\tt Test Printing Width.\optindex{Printing Width}} This command displays the current screen width used for display. -\subsection[\tt Set Printing Depth {\integer}.]{\tt Set Printing Depth {\integer}.\comindex{Set Printing Depth}} +\subsection[\tt Set Printing Depth {\integer}.]{\tt Set Printing Depth {\integer}.\optindex{Printing Depth}} This command sets the nesting depth of the formatter used for pretty-printing. Beyond this depth, display of subterms is replaced by dots. -\subsection[\tt Unset Printing Depth.]{\tt Unset Printing Depth.\comindex{Unset Printing Depth}} +\subsection[\tt Unset Printing Depth.]{\tt Unset Printing Depth.\optindex{Printing Depth}} This command resets the nesting depth of the formatter used for pretty-printing to its default value (at the time of writing this documentation, the default value is 50). -\subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\comindex{Test Printing Depth}} +\subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}} This command displays the current nesting depth used for display. %\subsection{\tt Abstraction ...} @@ -1146,17 +1063,17 @@ perform a {\tt Ltac \ident\ := {\rm\sl convtactic}}. \subsection{\tt Set Virtual Machine \label{SetVirtualMachine} -\comindex{Set Virtual Machine}} +\optindex{Virtual Machine}} This activates the bytecode-based conversion algorithm. \subsection{\tt Unset Virtual Machine -\comindex{Unset Virtual Machine}} +\optindex{Virtual Machine}} This deactivates the bytecode-based conversion algorithm. \subsection{\tt Test Virtual Machine -\comindex{Test Virtual Machine}} +\optindex{Virtual Machine}} This tells if the bytecode-based conversion algorithm is activated. The default behavior is to have the bytecode-based diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 08213abe9a..684a4add4c 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -400,13 +400,6 @@ This command displays the current goals. \item \errindex{No focused proof} \end{ErrMsgs} -\item {\tt Show Implicits.}\comindex{Show Implicits}\\ - Displays the current goals, printing the implicit arguments of - constants. - -\item {\tt Show Implicits {\num}.}\\ - Same as above, only displaying the {\num}-th subgoal. - \item {\tt Show Script.}\comindex{Show Script}\\ Displays the whole list of tactics applied from the beginning of the current proof. @@ -483,18 +476,18 @@ of the proof without having to wait the completion of the proof." \section{Controlling the effect of proof editing commands} -\subsection[\tt Set Hyps Limit {\num}.]{\tt Set Hyps Limit {\num}.\comindex{Set Hyps Limit}} +\subsection[\tt Set Hyps Limit {\num}.]{\tt Set Hyps Limit {\num}.\optindex{Hyps Limit}} This command sets the maximum number of hypotheses displayed in goals after the application of a tactic. All the hypotheses remains usable in the proof development. -\subsection[\tt Unset Hyps Limit.]{\tt Unset Hyps Limit.\comindex{Unset Hyps Limit}} +\subsection[\tt Unset Hyps Limit.]{\tt Unset Hyps Limit.\optindex{Hyps Limit}} This command goes back to the default mode which is to print all available hypotheses. -\subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\comindex{Set Automatic Introduction}\comindex{Unset Automatic Introduction}\label{Set Automatic Introduction}} +\subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\optindex{Automatic Introduction}\label{Set Automatic Introduction}} The option {\tt Automatic Introduction} controls the way binders are handled in assertion commands such as {\tt Theorem {\ident} diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 7d00a40059..571e16d578 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -123,12 +123,9 @@ The type of {\tt even\_odd} shares the same premises but the conclusion is {\tt (n:nat)(even n)->(Q n)}. \subsection{Automatic declaration of schemes -\comindex{Set Boolean Equality Schemes} -\comindex{Unset Boolean Equality Schemes} -\comindex{Set Elimination Schemes} -\comindex{Unset Elimination Schemes} -\comindex{Set Nonrecursive Elimination Schemes} -\comindex{Unset Nonrecursive Elimination Schemes} +\optindex{Boolean Equality Schemes} +\optindex{Elimination Schemes} +\optindex{Nonrecursive Elimination Schemes} \label{set-nonrecursive-elimination-schemes} } diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 24417bd039..15ddf62611 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -405,8 +405,7 @@ where "n + m" := (plus n m). \end{coq_example*} \subsection{Displaying informations about notations -\comindex{Set Printing Notations} -\comindex{Unset Printing Notations}} +\optindex{Printing Notations}} To deactivate the printing of all notations, use the command \begin{quote} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index ee40a0d51e..c3d8ad5318 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -55,7 +55,7 @@ selector (see Section \ref{default-selector}) is used. \end{tabular} \subsection[\tt Set Default Goal Selector ``\selector''.] {\tt Set Default Goal Selector ``\selector''. - \comindex{Set Default Goal Selector} + \optindex{Default Goal Selector} \label{default-selector}} After using this command, the default selector -- used when no selector is specified when applying a tactic -- is set to the chosen value. The @@ -66,8 +66,7 @@ simultaneously. Then, to apply a tactic {\tt tac} to the first goal only, you can write {\tt 1:tac}. \subsection[\tt Test Default Goal Selector.] - {\tt Test Default Goal Selector. - \comindex{Test Default Goal Selector}} + {\tt Test Default Goal Selector.} This command displays the current default selector. \subsection{Bindings list @@ -1789,9 +1788,19 @@ induction n. \item \texttt{induction {\term} in {\occgoalset}} This syntax is used for selecting which occurrences of {\term} the - induction has to be carried on. The {\tt in \occgoalset} clause is an - occurrence clause whose syntax and behavior is described in - Section~\ref{Occurrences_clauses}. + induction has to be carried on. The {\tt in \occgoalset} clause is + an occurrence clause whose syntax and behavior is described in + Section~\ref{Occurrences_clauses}. If variables or hypotheses not + mentioning {\term} in their type are listed in {\occgoalset}, those + are generalized as well in the statement to prove. + +\Example + +\begin{coq_example} +Lemma comm x y : x + y = y + x. +induction y in x |- *. +Show 2. +\end{coq_example} \item {\tt induction {\term$_1$} with {\bindinglist$_1$} as {\disjconjintropattern} %% eqn:{\namingintropattern} @@ -4133,7 +4142,7 @@ instead may reason about any first-order class inductive definition. \end{Variants} Proof-search is bounded by a depth parameter which can be set by typing the -{\nobreak \tt Set Firstorder Depth $n$} \comindex{Set Firstorder Depth} +{\nobreak \tt Set Firstorder Depth $n$} \optindex{Firstorder Depth} vernacular command. @@ -4878,7 +4887,6 @@ proof script in a non-sequential order. \section{Simple tactic macros} \index{Tactic macros} -\comindex{Tactic Definition} \label{TacticDefinition} A simple example has more value than a long explanation: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 91d30c0730..01ad0f70fa 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -143,6 +143,9 @@ Options A and B of the licence are {\em not} elected.} \printindex[command] \cutname{command-index.html} +\printindex[option] +\cutname{option-index.html} + \printindex[error] \cutname{error-index.html} diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 65218ba0dd..3414311148 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -106,7 +106,7 @@ in a universe strictly higher than \texttt{Set}. \asection{\tt Polymorphic, Monomorphic} \comindex{Polymorphic} \comindex{Monomorphic} -\comindex{Set Universe Polymorphism} +\optindex{Universe Polymorphism} As shown in the examples, polymorphic definitions and inductives can be declared using the \texttt{Polymorphic} prefix. There also exists an diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva index f65e1c10c1..df4aec272f 100644 --- a/doc/refman/headers.hva +++ b/doc/refman/headers.hva @@ -15,6 +15,10 @@ \protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}% Vernacular Commands Index} +\newindex{option}{optidx}{optind}{% +\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}% +Vernacular Options Index} + \newindex{error}{erridx}{errind}{% \protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages} @@ -26,6 +30,8 @@ Global Index} \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}} \newcommand{\comindex}[1]{% \index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}} +\newcommand{\optindex}[1]{% +\index{#1@\texttt{#1}}\index[option]{#1@\texttt{#1}}} \newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}} \newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}} \newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}} diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty index bc5f5c6c3f..ef28588e3c 100644 --- a/doc/refman/headers.sty +++ b/doc/refman/headers.sty @@ -39,6 +39,11 @@ \protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}% Vernacular Commands Index} +\newindex{option}{optidx}{optind}{% +\protect\setheaders{Vernacular Options Index}% +\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}% +Vernacular Options Index} + \newindex{error}{erridx}{errind}{% \protect\setheaders{Index of Error Messages}% \protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages} @@ -51,6 +56,8 @@ Vernacular Commands Index} \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}} \newcommand{\comindex}[1]{% \index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}} +\newcommand{\optindex}[1]{% +\index{#1@\texttt{#1}}\index[option]{#1@\texttt{#1}}} \newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}} \newcommand{\errindexbis}[2]{\texttt{#1}\index[error]{#2}} \newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}} diff --git a/doc/refman/menu.html b/doc/refman/menu.html index db19678f3c..7312ad344c 100644 --- a/doc/refman/menu.html +++ b/doc/refman/menu.html @@ -19,6 +19,9 @@ Tactics Index <TD><CENTER><A HREF="command-index.html" TARGET="UP"><FONT SIZE=2> Vernacular Commands Index </FONT></A></CENTER></TD> +<TD><CENTER><A HREF="option-index.html" TARGET="UP"><FONT SIZE=2> +Vernacular Options Index +</FONT></A></CENTER></TD> <TD><CENTER><A HREF="error-index.html" TARGET="UP"><FONT SIZE=2> Index of Error Messages </FONT></A></CENTER></TD> @@ -26,4 +29,4 @@ Index of Error Messages </CENTER> -</BODY></HTML>
\ No newline at end of file +</BODY></HTML> diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 6f474eb124..47612cdf72 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -247,7 +247,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "") ; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "") -; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "") (gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l") ; (gtk_accel_path "<Actions>/Tactics/Tactic right" "") ; (gtk_accel_path "<Actions>/Edit/Find Previous" "<Shift>F3") diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 689d4908f7..8ba1c8ecd2 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -218,8 +218,15 @@ object(self) let on_click id = let find _ _ s = Int.equal s.index id in let sentence = Doc.find document find in - let mark = sentence.stop in + let mark = sentence.start in let iter = script#buffer#get_iter_at_mark mark in + (** Sentence starts tend to be at the end of a line, so we rather choose + the first non-line-ending position. *) + let rec sentence_start iter = + if iter#ends_line then sentence_start iter#forward_line + else iter + in + let iter = sentence_start iter in script#buffer#place_cursor iter; ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter) in diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 995c45c5ae..37e38a5464 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -228,8 +228,6 @@ let state_preserving = [ "Test Printing Synth"; "Test Printing Wildcard"; - "Whelp Hint"; - "Whelp Locate"; ] diff --git a/ide/coqide.ml b/ide/coqide.ml index 5aac8f2a18..4564d620ea 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -852,6 +852,7 @@ let refresh_editor_prefs () = Tags.set_processing_color (Tags.color_of_string current.processing_color); Tags.set_processed_color (Tags.color_of_string current.processed_color); Tags.set_error_color (Tags.color_of_string current.error_color); + Tags.set_error_fg_color (Tags.color_of_string current.error_fg_color); sn.script#misc#modify_base [`NORMAL, `COLOR clr]; sn.proof#misc#modify_base [`NORMAL, `COLOR clr]; sn.messages#misc#modify_base [`NORMAL, `COLOR clr]; @@ -1149,14 +1150,14 @@ let build_ui () = menu templates_menu [ item "Templates" ~label:"Te_mplates"; - template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "L"); + template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "J"); template_item ("Theorem new_theorem : .\nProof.\n\nSave.\n", 8,11, "T"); template_item ("Definition ident := .\n", 11,5, "E"); template_item ("Inductive ident : :=\n | : .\n", 10,5, "I"); template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F"); template_item ("Scheme new_scheme := Induction for _ Sort _\n" ^ "with _ := Induction for _ Sort _.\n", 7,10, "S"); - item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"C") + item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"M") ~callback:match_callback ]; alpha_items templates_menu "Template" Coq_commands.commands; @@ -1164,13 +1165,12 @@ let build_ui () = let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in menu queries_menu [ item "Queries" ~label:"_Queries"; - qitem "Search" (Some "F2"); - qitem "Check" (Some "F3"); - qitem "Print" (Some "F4"); - qitem "About" (Some "F5"); - qitem "Locate" None; - qitem "Print Assumptions" None; - qitem "Whelp Locate" None; + qitem "Search" (Some "<Ctrl><Shift>K"); + qitem "Check" (Some "<Ctrl><Shift>C"); + qitem "Print" (Some "<Ctrl><Shift>P"); + qitem "About" (Some "<Ctrl><Shift>A"); + qitem "Locate" (Some "<Ctrl><Shift>L"); + qitem "Print Assumptions" (Some "<Ctrl><Shift>N"); ]; menu tools_menu [ @@ -1333,6 +1333,11 @@ let build_ui () = (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); Tags.Script.incomplete#set_property (`BACKGROUND_GDK (Tags.get_processed_color ())); + Tags.Script.read_only#set_property + (`BACKGROUND_STIPPLE + (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); + Tags.Script.read_only#set_property + (`BACKGROUND_GDK (Tags.get_processed_color ())); (* Showtime ! *) w#show () diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index af71b1e78c..edfe28b261 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -119,7 +119,6 @@ let init () = <menuitem action='About' /> <menuitem action='Locate' /> <menuitem action='Print Assumptions' /> - <menuitem action='Whelp Locate' /> </menu> <menu name='Tools' action='Tools'> <menuitem action='Comment' /> diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index abbd7e6d59..79ccf61a43 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -166,3 +166,16 @@ let find_nearest_backward (cursor:GText.iter) targets = | None -> raise Not_found | Some nearest -> nearest +(** On double-click on a view, select the whole word. This is a workaround for + a deficient word handling in TextView. *) +let fix_double_click self = + let callback ev = match GdkEvent.get_type ev with + | `TWO_BUTTON_PRESS -> + let iter = self#buffer#get_iter `INSERT in + let start, stop = get_word_around iter in + let () = self#buffer#move_mark `INSERT ~where:start in + let () = self#buffer#move_mark `SEL_BOUND ~where:stop in + true + | _ -> false + in + ignore (self#event#connect#button_press ~callback) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 84ef8f40db..473b8dc82e 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -132,8 +132,6 @@ let mktimer () = with Glib.GError _ -> ()); timer := None) } -let last_dir = ref "" - let filter_all_files () = GFile.filter ~name:"All" ~patterns:["*"] () @@ -142,6 +140,10 @@ let filter_coq_files () = GFile.filter ~name:"Coq source code" ~patterns:[ "*.v"] () +let current_dir () = match current.project_path with +| None -> "" +| Some dir -> dir + let select_file_for_open ~title () = let file = ref None in let file_chooser = @@ -152,14 +154,14 @@ let select_file_for_open ~title () = file_chooser#add_filter (filter_coq_files ()); file_chooser#add_filter (filter_all_files ()); file_chooser#set_default_response `OPEN; - ignore (file_chooser#set_current_folder !last_dir); + ignore (file_chooser#set_current_folder (current_dir ())); begin match file_chooser#run () with | `OPEN -> begin file := file_chooser#filename; match !file with | None -> () - | Some s -> last_dir := Filename.dirname s; + | Some s -> current.project_path <- file_chooser#current_folder end | `DELETE_EVENT | `CANCEL -> () end ; @@ -178,7 +180,7 @@ let select_file_for_save ~title ?filename () = file_chooser#set_do_overwrite_confirmation true; file_chooser#set_default_response `SAVE; let dir,filename = match filename with - |None -> !last_dir, "" + |None -> current_dir (), "" |Some f -> Filename.dirname f, Filename.basename f in ignore (file_chooser#set_current_folder dir); @@ -189,7 +191,7 @@ let select_file_for_save ~title ?filename () = file := file_chooser#filename; match !file with None -> () - | Some s -> last_dir := Filename.dirname s; + | Some s -> current.project_path <- file_chooser#current_folder end | `DELETE_EVENT | `CANCEL -> () end ; diff --git a/ide/preferences.ml b/ide/preferences.ml index 9a4fde2f6e..c59642d3a7 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -105,6 +105,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; + mutable project_path : string option; mutable encoding : inputenc; @@ -180,8 +181,9 @@ let current = { source_language = "coq"; source_style = "coq_style"; - read_project = Ignore_args; + read_project = Append_args; project_file_name = "_CoqProject"; + project_path = None; encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale; @@ -265,6 +267,7 @@ let save_pref () = add "project_options" [string_of_project_behavior p.read_project] ++ add "project_file_name" [p.project_file_name] ++ + add "project_path" (match p.project_path with None -> [] | Some s -> [s]) ++ add "encoding" [string_of_inputenc p.encoding] ++ @@ -342,6 +345,7 @@ let load_pref () = set_hd "project_options" (fun v -> np.read_project <- (project_behavior_of_string v)); set_hd "project_file_name" (fun v -> np.project_file_name <- v); + set_option "project_path" (fun v -> np.project_path <- v); set "automatic_tactics" (fun v -> np.automatic_tactics <- v); set_hd "cmd_print" (fun v -> np.cmd_print <- v); diff --git a/ide/preferences.mli b/ide/preferences.mli index ab12e4c7ba..1e4f152c23 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -32,6 +32,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; + mutable project_path : string option; mutable encoding : inputenc; diff --git a/ide/tags.ml b/ide/tags.ml index 079cf94853..d4460b0770 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -52,7 +52,9 @@ struct t let all = edit_zone :: all - let read_only = make_tag table ~name:"read_only" [`EDITABLE false ] + let read_only = make_tag table ~name:"read_only" [`EDITABLE false; + `BACKGROUND !processing_color; + `BACKGROUND_STIPPLE_SET true ] end module Proof = @@ -94,6 +96,7 @@ let set_processing_color clr = let s = string_of_color clr in processing_color := s; Script.incomplete#set_property (`BACKGROUND s); + Script.read_only#set_property (`BACKGROUND s); Script.to_process#set_property (`BACKGROUND s) let get_error_color () = color_of_string !error_color diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 09f1d44535..b32674084d 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -48,6 +48,7 @@ let message_view () : message_view = ~source_buffer:buffer ~packing:scroll#add ~editable:false ~cursor_visible:false ~wrap_mode:`WORD () in + let () = Gtk_parsing.fix_double_click view in let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in let () = view#set_left_margin 2 in diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index a33f2c591c..b12d29d6c9 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -181,6 +181,7 @@ let proof_view () = let view = GSourceView2.source_view ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD () in + let () = Gtk_parsing.fix_double_click view in let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in object diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 5d21efd956..8298d9954f 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -418,6 +418,7 @@ object (self) self#buffer#end_user_action () initializer + let () = Gtk_parsing.fix_double_click self in let supersed cb _ = let _ = cb () in GtkSignal.stop_emit() diff --git a/library/assumptions.ml b/library/assumptions.ml index 04ee14fb53..ab07b3647e 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -205,7 +205,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> (iter_array e1_array) ** (iter_array e2_array) | Const (kn,_) -> do_memoize_kn kn - | _ -> identity2 (* closed atomic types + rel *) + | Proj (_, e) -> iter e + | Rel _ | Sort _ | Ind _ | Construct _ -> identity2 and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2 in iter t s acc diff --git a/library/global.mli b/library/global.mli index af23d9b72c..62d7ea3210 100644 --- a/library/global.mli +++ b/library/global.mli @@ -118,9 +118,23 @@ val is_template_polymorphic : Globnames.global_reference -> bool val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types Univ.in_universe_context -val type_of_global_unsafe : Globnames.global_reference -> Constr.types +(** Returns the type of the constant in its global or local universe + context. The type should not be used without pushing it's universe + context in the environmnent of usage. For non-universe-polymorphic + constants, it does not matter. *) -(** Returns the universe context of the global reference (whatever it's polymorphic status is). *) +val type_of_global_unsafe : Globnames.global_reference -> Constr.types +(** Returns the type of the constant, forgetting its universe context if + it is polymorphic, use with care: for polymorphic constants, the + type cannot be used to produce a term used by the kernel. For safe + handling of polymorphic global references, one should look at a + particular instantiation of the reference, in some particular + universe context (part of an [env] or [evar_map]), see + e.g. [type_of_constant_in]. If you want to create a fresh instance + of the reference and get its type look at [Evd.fresh_global] or + [Evarutil.new_global] and [Retyping.get_type_of]. *) + +(** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : Globnames.global_reference -> Univ.universe_context (** {6 Retroknowledge } *) diff --git a/library/goptions.ml b/library/goptions.ml index 4aea33685e..ef25fa5902 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -268,10 +268,14 @@ let declare_option cast uncast begin fun v -> add_anonymous_leaf (gdecl_obj v) end else write,write,write in + let warn () = + if depr then + msg_warning (str "Option " ++ str (nickname key) ++ str " is deprecated") + in let cread () = cast (read ()) in - let cwrite v = write (uncast v) in - let clwrite v = lwrite (uncast v) in - let cgwrite v = gwrite (uncast v) in + let cwrite v = warn (); write (uncast v) in + let clwrite v = warn (); lwrite (uncast v) in + let cgwrite v = warn (); gwrite (uncast v) in value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab; write diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 040792ef53..e3dba232b2 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -324,12 +324,6 @@ let pretype_id pretype loc env evdref lvar id = (* Check if [id] is a section or goal variable *) try let (_,_,typ) = lookup_named id env in - (* let _ = *) - (* try *) - (* let ctx = Decls.variable_context id in *) - (* evdref := Evd.merge_context_set univ_rigid !evdref ctx; *) - (* with Not_found -> () *) - (* in *) { uj_val = mkVar id; uj_type = typ } with Not_found -> (* [id] not found, standard error message *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index b64ccf60dd..18e83056bd 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -483,15 +483,6 @@ let is_instance = function is_class (IndRef ind) | _ -> false -let is_implicit_arg = function -| Evar_kinds.GoalEvar -> false -| _ -> true - (* match k with *) - (* ImplicitArg (ref, (n, id), b) -> true *) - (* | InternalHole -> true *) - (* | _ -> false *) - - (* To embed a boolean for resolvability status. This is essentially a hack to mark which evars correspond to goals and do not need to be resolved when we have nested [resolve_all_evars] diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 1a0b6696a8..b3170b9702 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -77,8 +77,6 @@ val instance_priority : instance -> int option val is_class : global_reference -> bool val is_instance : global_reference -> bool -val is_implicit_arg : Evar_kinds.t -> bool - (** Returns the term and type for the given instance of the parameters and fields of the type class. *) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 672527d9b5..e3fb0b607a 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -177,7 +177,7 @@ module Make(T : Task) = struct if not (Worker.is_alive proc) then () else if cancelled () || !(!expiration_date) then let () = stop_waiting := true in - let () = TQueue.signal_destruction queue in + let () = TQueue.broadcast queue in Worker.kill proc else let () = Unix.sleep 1 in @@ -253,6 +253,8 @@ module Make(T : Task) = struct Pool.destroy active; TQueue.destroy queue + let broadcast { queue } = TQueue.broadcast queue + let enqueue_task { queue; active } (t, _ as item) = prerr_endline ("Enqueue task "^T.name_of_task t); TQueue.push queue item diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index 78f295d3d5..a3fe4b8c0d 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -61,6 +61,8 @@ module MakeQueue(T : Task) : sig val set_order : queue -> (T.task -> T.task -> int) -> unit + val broadcast : queue -> unit + (* Take a snapshot (non destructive but waits until all workers are * enqueued) *) val snapshot : queue -> T.task list diff --git a/stm/stm.ml b/stm/stm.ml index 207afd8aee..43db6f3f6c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -132,6 +132,7 @@ type branch_type = | `Proof of proof_mode * depth | `Edit of proof_mode * Stateid.t * Stateid.t ] type cmd_t = { + ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *) cast : ast; cids : Id.t list; cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] } @@ -144,7 +145,7 @@ type qed_t = { brinfo : branch_type Vcs_.branch_info } type seff_t = ast option -type alias_t = Stateid.t +type alias_t = Stateid.t * ast type transaction = | Cmd of cmd_t | Fork of fork_t @@ -315,7 +316,7 @@ end = struct (* {{{ *) (try string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff None -> "EnvChange" | Noop -> " " - | Alias id -> sprintf "Alias(%s)" (Stateid.to_string id) + | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id) | Qed { qast } -> string_of_ppcmds (pr_ast qast) in let is_green id = match get_info vcs id with @@ -769,19 +770,20 @@ end = struct (* {{{ *) match info.vcs_backup with | None, _ -> next acc | Some vcs, _ -> - let ids = - if id = Stateid.initial || id = Stateid.dummy then [] else + let ids, tactic, undo = + if id = Stateid.initial || id = Stateid.dummy then [],false,0 else match VCS.visit id with - | { step = `Fork ((_,_,_,l),_) } -> l - | { step = `Cmd { cids = l } } -> l - | _ -> [] in - match f acc (id, vcs, ids) with + | { step = `Fork ((_,_,_,l),_) } -> l, false,0 + | { step = `Cmd { cids = l; ctac } } -> l, ctac,0 + | { step = `Alias (_,{ expr = VernacUndo n}) } -> [], false, n + | _ -> [],false,0 in + match f acc (id, vcs, ids, tactic, undo) with | `Stop x -> x | `Cont acc -> next acc let back_safe () = let id = - fold_until (fun n (id,_,_) -> + fold_until (fun n (id,_,_,_,_) -> if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n)) 0 (VCS.get_branch_pos (VCS.current_branch ())) in backto id @@ -797,7 +799,7 @@ end = struct (* {{{ *) let id = VCS.get_branch_pos (VCS.current_branch ()) in (try let oid = - fold_until (fun b (id,_,label) -> + fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in VtStm (VtBack oid, true), VtNow @@ -805,17 +807,15 @@ end = struct (* {{{ *) VtStm (VtBack id, true), VtNow) | VernacBack n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun n (id,_,_) -> + let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in VtStm (VtBack oid, true), VtNow | VernacUndo n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun n (id,_,_) -> - if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode && - not !Flags.print_emacs then - VtStm (VtBack oid, false), VtNow - else VtStm (VtBack oid, true), VtLater + let oid = fold_until (fun n (id,_,_,tactic,undo) -> + let value = (if tactic then 1 else 0) - undo in + if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in + VtStm (VtBack oid, true), VtLater | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in @@ -826,15 +826,15 @@ end = struct (* {{{ *) | Some vcs, _ -> vcs in let cb, _ = Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in - let n = fold_until (fun n (_,vcs,_) -> + let n = fold_until (fun n (_,vcs,_,_,_) -> if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) 0 id in - let oid = fold_until (fun n (id,_,_) -> + let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in VtStm (VtBack oid, true), VtLater | VernacAbortAll -> let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun () (id,vcs,_) -> + let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in VtStm (VtBack oid, true), VtLater @@ -907,7 +907,10 @@ module rec ProofTask : sig val build_proof_here : Stateid.t * Stateid.t -> Loc.t -> Stateid.t -> Proof_global.closed_proof_output Future.computation - + + (* If set, only tasks overlapping with this list are processed *) + val set_perspective : Stateid.t list -> unit + end = struct (* {{{ *) let forward_feedback msg = Hooks.(call forward_feedback msg) @@ -946,9 +949,14 @@ end = struct (* {{{ *) let name = ref "proofworker" let extra_env () = !async_proofs_workers_extra_env + let perspective = ref [] + let set_perspective l = perspective := l + let task_match age t = match age, t with - | `Fresh, BuildProof _ -> true + | `Fresh, BuildProof { t_states } -> + not !Flags.async_proofs_full || + List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) t_states | `Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l | _ -> false @@ -1239,6 +1247,8 @@ end = struct (* {{{ *) name, max (time1 +. time2) 0.0001,i) 0 l let set_perspective idl = + ProofTask.set_perspective idl; + TaskQueue.broadcast (Option.get !queue); let open Stateid in let open ProofTask in let overlap s1 s2 = @@ -1667,7 +1677,7 @@ let known_state ?(redefine_qed=false) ~cache id = let step, cache_step, feedback_processed = let view = VCS.visit id in match view.step with - | `Alias id -> (fun () -> + | `Alias (id,_) -> (fun () -> reach view.next; reach id ), cache, true | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () -> @@ -1968,11 +1978,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = List.iter (fun b -> if not(VCS.Branch.equal b head) then begin VCS.checkout b; - VCS.commit (VCS.new_node ()) (Alias oid); + VCS.commit (VCS.new_node ()) (Alias (oid,x)); end) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); - VCS.commit id (Alias oid); + VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok | VtStm (VtBack id, false), VtNow -> prerr_endline ("undo to state " ^ Stateid.to_string id); @@ -2001,7 +2011,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) else `MainQueue in - VCS.commit id (Cmd { cast = x; cids = []; cqueue = queue }); + VCS.commit id (Cmd {ctac=false;cast = x; cids = []; cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQuery (false,_), VtLater -> anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") @@ -2025,7 +2035,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; - VCS.commit id (Cmd {cast = x; cids=[]; cqueue = `MainQueue}); + VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue}); VCS.propagate_sideff (Some x); List.iter (fun bn -> match VCS.get_branch bn with @@ -2044,7 +2054,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtProofStep paral, w -> let id = VCS.new_node ~id:newtip () in let queue = if paral then `TacQueue (ref false) else `MainQueue in - VCS.commit id (Cmd {cast = x; cids = []; cqueue = queue }); + VCS.commit id (Cmd {ctac = true;cast = x;cids = [];cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> let valid = if tty then Some(VCS.get_branch_pos head) else None in @@ -2060,7 +2070,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtSideff l, w -> let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; - VCS.commit id (Cmd { cast = x; cids = l; cqueue = `MainQueue}); + VCS.commit id (Cmd {ctac=false;cast=x;cids=l;cqueue=`MainQueue}); VCS.propagate_sideff (Some x); VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); `Ok @@ -2084,7 +2094,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode "Classic"; end else begin - VCS.commit id (Cmd { cast = x; cids = []; cqueue = `MainQueue}); + VCS.commit id (Cmd {ctac=false; cast = x; cids = []; cqueue = `MainQueue}); VCS.propagate_sideff (Some x); VCS.checkout_shallowest_proof_branch (); end in @@ -2332,7 +2342,7 @@ let get_script prf = find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next | `Sideff (`Id id) -> find acc id | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Alias id -> find acc id + | `Alias (id,_) -> find acc id | `Fork _ -> find acc view.next in find [] (VCS.get_branch_pos branch) diff --git a/stm/tQueue.ml b/stm/tQueue.ml index 8a62fe79e1..6fef895ae8 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -79,7 +79,7 @@ let pop ?(picky=(fun _ -> true)) ?(destroy=ref false) Mutex.unlock m; x -let signal_destruction { lock = m; cond = c } = +let broadcast { lock = m; cond = c } = Mutex.lock m; Condition.broadcast c; Mutex.unlock m diff --git a/stm/tQueue.mli b/stm/tQueue.mli index bc3922b33a..7458de510f 100644 --- a/stm/tQueue.mli +++ b/stm/tQueue.mli @@ -14,7 +14,9 @@ val pop : ?picky:('a -> bool) -> ?destroy:bool ref -> 'a t -> 'a val push : 'a t -> 'a -> unit val set_order : 'a t -> ('a -> 'a -> int) -> unit val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit -val signal_destruction : 'a t -> unit + +(* Wake up all waiting threads *) +val broadcast : 'a t -> unit (* Non destructive *) val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index e9302bb735..81fad13793 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -151,8 +151,8 @@ let rec classify_vernac e = let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in VtSideff ids, VtLater | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater + | VernacBeginSection (_,id) -> VtSideff [id], VtLater | VernacUniverse _ | VernacConstraint _ - | VernacBeginSection _ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ | VernacChdir _ diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 9289c6d663..ac8b4923e5 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -283,7 +283,7 @@ end) = struct (app_poly env evd arrow [| a; b |]), unfold_impl (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) - (app_poly env evd coq_all [| a; mkLambda (Anonymous, a, b) |]), unfold_forall + (app_poly env evd coq_all [| a; mkLambda (Anonymous, a, lift 1 b) |]), unfold_forall else (* None in Prop, use arrow *) (app_poly env evd arrow [| a; b |]), unfold_impl @@ -1444,7 +1444,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let newt = Evarutil.nf_evar evars' res.rew_to in let evars = (* Keep only original evars (potentially instantiated) and goal evars, the rest has been defined and substituted already. *) - Evar.Set.fold (fun ev acc -> Evd.remove acc ev) cstrs evars' + Evar.Set.fold + (fun ev acc -> + if not (Evd.is_defined acc ev) then + errorlabstrm "rewrite" + (str "Unsolved constraint remaining: " ++ spc () ++ + Evd.pr_evar_info (Evd.find acc ev)) + else Evd.remove acc ev) + cstrs evars' in let res = match res.rew_prf with | RewCast c -> None diff --git a/test-suite/bugs/closed/2946.v b/test-suite/bugs/closed/2946.v new file mode 100644 index 0000000000..d8138e145c --- /dev/null +++ b/test-suite/bugs/closed/2946.v @@ -0,0 +1,8 @@ +Lemma toto (E : nat -> nat -> Prop) (x y : nat) + (Ex_ : forall z, E x z) (E_y : forall z, E z y) : True. + +(* OK *) +assert (pairE1 := let Exy := _ in (Ex_ y, E_y _) : Exy * Exy). + +(* FAIL *) +assert (pairE2 := let Exy := _ in (Ex_ _, E_y x) : Exy * Exy). diff --git a/test-suite/bugs/closed/3703.v b/test-suite/bugs/closed/3703.v new file mode 100644 index 0000000000..8f7fe0a09f --- /dev/null +++ b/test-suite/bugs/closed/3703.v @@ -0,0 +1,31 @@ +(* File reduced by coq-bug-finder from original input, then from 6746 lines to 4190 lines, then from 29 lines to 18 lines, then fro\ +m 30 lines to 19 lines *) +(* coqc version trunk (October 2014) compiled on Oct 7 2014 12:42:41 with OCaml 4.01.0 + coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (2313bde0116a5916912bebbaca77d291f7b2760a) *) +Record PreCategory := { identity : forall x, x -> x }. +Definition set_cat : PreCategory := @Build_PreCategory (fun T x => x). +Module UnKeyed. + Global Unset Keyed Unification. + Goal forall (T : Type) (g0 g1 : T) (k : T) (H' : forall x : T, k = @identity set_cat T x), + ((fun x : T => x) g0) = ((fun x : T => x) g1). + intros T g0 g1 k H'. + change (identity _ _) with (fun y : T => y) in H'; + rewrite <- H' || fail "too early". + Undo. + rewrite <- H'. + admit. + Defined. +End UnKeyed. +Module Keyed. + Global Set Keyed Unification. + Declare Equivalent Keys (fun x => _) identity. + Goal forall (T : Type) (g0 g1 : T) (k : T) (H' : forall x : T, k = @identity set_cat T x), + ((fun x : T => x) g0) = ((fun x : T => x) g1). + intros T g0 g1 k H'. + change (identity _ _) with (fun y : T => y) in H'; + rewrite <- H' || fail "too early". + Undo. + rewrite <- H'. + admit. + Defined. +End Keyed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v new file mode 100644 index 0000000000..6b52411752 --- /dev/null +++ b/test-suite/bugs/closed/3922.v @@ -0,0 +1,83 @@ +Set Universe Polymorphism. +Notation Type0 := Set. + +Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. +Open Scope function_scope. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. +Local Open Scope trunc_scope. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | -2 => Contr_internal A + | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. + +Notation Contr := (IsTrunc -2). +Notation IsHProp := (IsTrunc -1). + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Inductive Unit : Type1 := + tt : Unit. + +Record TruncType (n : trunc_index) := BuildTruncType { + trunctype_type : Type ; + istrunc_trunctype_type : IsTrunc n trunctype_type +}. + +Arguments BuildTruncType _ _ {_}. + +Coercion trunctype_type : TruncType >-> Sortclass. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (-1)-Type. + +Notation BuildhProp := (BuildTruncType -1). + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + +Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i}) +: IsTrunc@{j} n (Trunc@{i} n A). +Admitted. + +Definition Trunc_ind {n A} + (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} + : (forall a, P (tr a)) -> (forall aa, P aa) +:= (fun f aa => match aa with tr a => fun _ => f a end Pt). +Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). +Definition cconst_factors_contr `{Funext} {X Y : Type} (f : X -> Y) + (P : Type) `{Pc : X -> Contr P} + (g : X -> P) (h : P -> Y) (p : h o g == f) +: Unit. +Proof. + assert (merely X -> IsHProp P) by admit. + refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _); + [ assumption.. | ]. + pose (g'' := Trunc_ind (fun _ => P) g : merely X -> P). diff --git a/test-suite/bugs/closed/3938.v b/test-suite/bugs/closed/3938.v new file mode 100644 index 0000000000..9844313383 --- /dev/null +++ b/test-suite/bugs/closed/3938.v @@ -0,0 +1,7 @@ +Require Import Coq.Arith.PeanoNat. +Hint Extern 1 => admit : typeclass_instances. +Require Import Setoid. +Goal forall a b (f : nat -> Set) (R : nat -> nat -> Prop), + Equivalence R -> R a b -> f a = f b. + intros a b f H. + intros. Fail rewrite H1. diff --git a/test-suite/bugs/closed/3944.v b/test-suite/bugs/closed/3944.v new file mode 100644 index 0000000000..58e60f4f2e --- /dev/null +++ b/test-suite/bugs/closed/3944.v @@ -0,0 +1,5 @@ +Require Import Setoid. +Definition C (T : Type) := T. +Goal forall T (i : C T) (v : T), True. +Proof. +Fail setoid_rewrite plus_n_Sm. diff --git a/test-suite/bugs/closed/3960.v b/test-suite/bugs/closed/3960.v new file mode 100644 index 0000000000..e56dcef74f --- /dev/null +++ b/test-suite/bugs/closed/3960.v @@ -0,0 +1,26 @@ +Require Program.Tactics. + +Axiom foo : nat -> Prop. + +Axiom fooP : forall n, foo n. + +Class myClass (A: Type) := + { + bar : A -> Prop + }. + +Program Instance myInstance : myClass nat := + { + bar := foo + }. + +Class myClassP (A : Type) := + { + super :> myClass A; + barP : forall (a : A), bar a + }. + +Instance myInstanceP : myClassP nat := + { + barP := fooP + }.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4035.v b/test-suite/bugs/closed/4035.v new file mode 100644 index 0000000000..24f340bbd9 --- /dev/null +++ b/test-suite/bugs/closed/4035.v @@ -0,0 +1,7 @@ +(* Use of dependent destruction from ltac *) +Require Import Program. +Goal nat -> Type. + intro x. + lazymatch goal with + | [ x : nat |- _ ] => dependent destruction x + end. diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v index 89638eedd7..5f1926f142 100644 --- a/test-suite/output/simpl.v +++ b/test-suite/output/simpl.v @@ -4,10 +4,10 @@ Goal forall x, 0+x = 1+x. intro x. simpl (_ + x). Show. -Undo 2. +Undo. simpl (_ + x) at 2. Show. -Undo 2. +Undo. simpl (0 + _). Show. -Undo 2. +Undo. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index ae6fe7dd0a..4b02873172 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -433,40 +433,40 @@ Ltac do_depelim' rev tac H := (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. By default, we don't try to generalize the hyp by its variable indices. *) -Tactic Notation "dependent" "destruction" ident(H) := +Tactic Notation "dependent" "destruction" hyp(H) := do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => do_case hyp) H. -Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := +Tactic Notation "dependent" "destruction" hyp(H) "using" constr(c) := do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => destruct hyp using c) H. (** This tactic also generalizes the goal by the given variables before the elimination. *) -Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := +Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) := do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_case hyp) H. -Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := +Tactic Notation "dependent" "destruction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H. (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before calling [induction]. *) -Tactic Notation "dependent" "induction" ident(H) := +Tactic Notation "dependent" "induction" hyp(H) := do_depind ltac:(fun hyp => do_ind hyp) H. -Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := +Tactic Notation "dependent" "induction" hyp(H) "using" constr(c) := do_depind ltac:(fun hyp => induction hyp using c) H. (** This tactic also generalizes the goal by the given variables before the induction. *) -Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := +Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) := do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => do_ind hyp) H. -Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := +Tactic Notation "dependent" "induction" hyp(H) "generalizing" ne_hyp_list(l) "using" constr(c) := do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => induction hyp using c) H. -Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) := +Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) := do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l) H. -Tactic Notation "dependent" "induction" ident(H) "in" ne_hyp_list(l) "using" constr(c) := +Tactic Notation "dependent" "induction" hyp(H) "in" ne_hyp_list(l) "using" constr(c) := do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => induction hyp in l using c) H. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index f44ac36788..07f881721d 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -165,7 +165,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro in let env' = push_rel_context ctx env in evars := Evarutil.nf_evar_map !evars; - evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env !evars; + evars := resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env !evars; let subst = List.map (Evarutil.nf_evar !evars) subst in if abstract then begin @@ -208,7 +208,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro let get_id = function | Ident id' -> id' - | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled") + | Qualid (loc,id') -> (loc, snd (repr_qualid id')) in let props, rest = List.fold_left @@ -232,7 +232,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro k.cl_projs; c :: props, rest' with Not_found -> - (CHole (Loc.ghost, Some Evar_kinds.GoalEvar, Misctypes.IntroAnonymous, None) :: props), rest + (CHole (Loc.ghost, None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None) :: props), rest else props, rest) ([], props) k.cl_props in diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d22524e5ca..bf0f305abd 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -13,7 +13,6 @@ Record Vernacinterp Mltop Vernacentries -Whelp Vernac Usage Coqloop diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 deleted file mode 100644 index daedc30f42..0000000000 --- a/toplevel/whelp.ml4 +++ /dev/null @@ -1,224 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "grammar/grammar.cma" i*) - -open Flags -open Pp -open Errors -open Names -open Term -open Glob_term -open Libnames -open Globnames -open Nametab -open Detyping -open Constrintern -open Dischargedhypsmap -open Pfedit -open Tacmach -open Misctypes - -(* Coq interface to the Whelp query engine developed at - the University of Bologna *) - -let whelp_server_name = ref "http://mowgli.cs.unibo.it:58080" -let getter_server_name = ref "http://mowgli.cs.unibo.it:58081" - -open Goptions - -let _ = - declare_string_option - { optsync = false; - optdepr = false; - optname = "Whelp server"; - optkey = ["Whelp";"Server"]; - optread = (fun () -> !whelp_server_name); - optwrite = (fun s -> whelp_server_name := s) } - -let _ = - declare_string_option - { optsync = false; - optdepr = false; - optname = "Whelp getter"; - optkey = ["Whelp";"Getter"]; - optread = (fun () -> !getter_server_name); - optwrite = (fun s -> getter_server_name := s) } - - -let make_whelp_request req c = - !whelp_server_name ^ "/apply?xmluri=" ^ !getter_server_name ^ "/getempty¶m.profile=firewall&profile=firewall¶m.keys=d_c%2CC1%2CHC2%2CL¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thkeys=T1%2CT2%2CL%2CE¶m.prooftreekeys=HAT%2CG%2CHAO%2CL¶m.media-type=text%2Fhtml¶m.thmedia-type=&prooftreemedia-type=¶m.doctype-public=¶m.encoding=¶m.thencoding=¶m.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE¶m.expression=" ^ c ^ "¶m.action=" ^ req - -let b = Buffer.create 16 - -let url_char c = - if 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' || - '0' <= c && c <= '9' || c ='.' - then Buffer.add_char b c - else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c)) - -let url_string s = String.iter url_char s - -let rec url_list_with_sep sep f = function - | [] -> () - | [a] -> f a - | a::l -> f a; url_string sep; url_list_with_sep sep f l - -let url_id id = url_string (Id.to_string id) - -let uri_of_dirpath dir = - url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir) - -let error_whelp_unknown_reference ref = - let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in - errorlabstrm "" - (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++ - strbrk ", are not supported in Whelp.") - -let uri_of_repr_kn ref (mp,dir,l) = - match mp with - | MPfile sl -> - uri_of_dirpath (Label.to_id l :: DirPath.repr dir @ DirPath.repr sl) - | _ -> - error_whelp_unknown_reference ref - -let url_paren f l = url_char '('; f l; url_char ')' -let url_bracket f l = url_char '['; f l; url_char ']' - -let whelp_of_glob_sort = function - | GProp -> "Prop" - | GSet -> "Set" - | GType _ -> "Type" - -let uri_int n = Buffer.add_string b (string_of_int n) - -let uri_of_ind_pointer l = - url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l - -let uri_of_global ref = - match ref with - | VarRef id -> error ("Unknown Whelp reference: "^(Id.to_string id)^".") - | ConstRef cst -> - uri_of_repr_kn ref (repr_con cst); url_string ".con" - | IndRef (kn,i) -> - uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1] - | ConstructRef ((kn,i),j) -> - uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1;j] - -let whelm_special = Id.of_string "WHELM_ANON_VAR" - -let url_of_name = function - | Name id -> url_id id - | Anonymous -> url_id whelm_special (* No anon id in Whelp *) - -let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c - -let uri_params f = function - | [] -> () - | l -> url_string "\\subst"; - url_bracket (url_list_with_sep ";" (uri_of_binding f)) l - -let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp) - -let section_parameters = function - | GRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_)),_) -> - get_discharged_hyp_names (path_of_global (IndRef(induri,0))) - | GRef (_,(ConstRef cst as ref),_) -> - get_discharged_hyp_names (path_of_global ref) - | _ -> [] - -let merge vl al = - let rec aux acc = function - | ([],l) | (_,([] as l)) -> List.rev acc, l - | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al) - in aux [] (vl,al) - -let rec uri_of_constr c = - match c with - | GVar (_,id) -> url_id id - | GRef (_,ref,_) -> uri_of_global ref - | GHole _ | GEvar _ -> url_string "?" - | GSort (_,s) -> url_string (whelp_of_glob_sort s) - | GApp (_,f,args) -> - let inst,rest = merge (section_parameters f) args in - uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; - url_list_with_sep " " uri_of_constr rest - | GLambda (_,na,k,ty,c) -> - url_string "\\lambda "; url_of_name na; url_string ":"; - uri_of_constr ty; url_string "."; uri_of_constr c - | GProd (_,Anonymous,k,ty,c) -> - uri_of_constr ty; url_string "\\to "; uri_of_constr c - | GProd (_,Name id,k,ty,c) -> - url_string "\\forall "; url_id id; url_string ":"; - uri_of_constr ty; url_string "."; uri_of_constr c - | GLetIn (_,na,b,c) -> - url_string "let "; url_of_name na; url_string "\\def "; - uri_of_constr b; url_string " in "; uri_of_constr c - | GCast (_,c, (CastConv t|CastVM t|CastNative t)) -> - uri_of_constr c; url_string ":"; uri_of_constr t - | GRec _ | GIf _ | GLetTuple _ | GCases _ -> - error "Whelp does not support pattern-matching and (co-)fixpoint." - | GCast (_,_, CastCoerce) -> - anomaly (Pp.str "Written w/o parenthesis") - | GPatVar _ -> - anomaly (Pp.str "Found constructors not supported in constr") - -let make_string f x = Buffer.reset b; f x; Buffer.contents b - -let send_whelp req s = - let url = make_whelp_request req s in - let command = Util.subst_command_placeholder browser_cmd_fmt url in - let _ = CUnix.run_command ~hook:print_string command in () - -let whelp_constr env sigma req c = - let c = detype false [whelm_special] env sigma c in - send_whelp req (make_string uri_of_constr c) - -let whelp_constr_expr req c = - let (sigma,env)= Lemmas.get_current_context () in - let _,c = interp_open_constr env sigma c in - whelp_constr env sigma req c - -let whelp_locate s = - send_whelp "locate" s - -let whelp_elim ind = - send_whelp "elim" (make_string uri_of_global (IndRef ind)) - -let on_goal f = - let gls = Proof.V82.subgoals (get_pftreestate ()) in - let gls = { gls with Evd.it = List.hd gls.Evd.it } in - f (pf_env gls) (project gls) (Termops.it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) - -type whelp_request = - | Locate of string - | Elim of inductive - | Constr of string * constr - -let whelp = function - | Locate s -> whelp_locate s - | Elim ind -> whelp_elim ind - | Constr (s,c) -> whelp_constr (Global.env()) (Evd.empty) s c - -VERNAC ARGUMENT EXTEND whelp_constr_request -| [ "Match" ] -> [ "match" ] -| [ "Instance" ] -> [ "instance" ] -END - -VERNAC COMMAND EXTEND Whelp CLASSIFIED AS QUERY -| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] -| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ] -| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] -END - -VERNAC COMMAND EXTEND WhelpHint CLASSIFIED AS QUERY -| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] -| [ "Whelp" "Hint" ] => [ Vernacexpr.VtProofStep false, Vernacexpr.VtLater ] -> - [ on_goal (fun env sigma -> whelp_constr env sigma "hint") ] -END diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli deleted file mode 100644 index 62272c50ff..0000000000 --- a/toplevel/whelp.mli +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Coq interface to the Whelp query engine developed at - the University of Bologna *) - -open Names -open Term - -type whelp_request = - | Locate of string - | Elim of inductive - | Constr of string * constr - -val whelp : whelp_request -> unit |