| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Was PR#294: Make error message more helpful.
|
|
Was PR#257: [checker] Fix/fine tune printing.
|
|
|
|
We use the same printing path for color and mono terminal output, thus
removing the duplicate printers which avoids problems as they don't have
to be kept in sync anymore.
We tag unconditionally but set the `pp_tag` tagger properly. This
removes IO from `Ppstyle` with IMO is the right thing to do.
Test suite passes.
|
|
Was PR#293: Fix #4762 (eauto weaker than auto).
|
|
|
|
|
|
This was the original value from Tobias' code. When a user passes
-profile-ltac on the command line, or inserts [Show Ltac Profile] in the
document, the most useful default behavior is to not overload them with
useless information. When GUI clients want to display fancier profiling
information, there is no cost to the user to requiring them to specify
what cutoff they want. If the GUI client does not have any special
LtacProf handling, the most useful presentation is again the one that
cuts off the display at 2% total time.
|
|
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations
no longer modify the parser in non-compat-mode, so we can do this
without breaking Ltac parsing. Also update the related test-suite
files.
|
|
This is a quick fix. The Metasyntax module should be thoroughly revised
in trunk, because it starts featuring a lot of spaghetti code and redundant
data.
|
|
When a proof is 're-opened', the Qed node does not change.
Still the STM has to install the old state (where only
the future proof has to be updated). This bit was missing.
Why was it working: the bug happens only if you
reopen the very last proof, i.e. there is no
sentence that stays valid after the Qed. If there
is such a sentence, its state was computed correctly
before, and is not changed. If it is the very last,
then the next state is based on the wrong one...
|
|
It seems warnings are not taken into account in output/
tests.
|
|
|
|
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
|
|
|
|
|
|
|
|
in error messages
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
With this command line flag one can profile ltac in files
/and/ trim the results without actually touching the files.
|
|
|
|
|
|
|
|
This avoids leakage of universes. Also makes
Program Lemma/Fact work again, it tries to solve the
remaining evars using the obligation tactic.
|
|
When inserting a character in an already processed buffer, a message is
sent to Coq so that the proof is backtracked and the character is
inserted. If a second character is inserted while Coq is still busy with
the first message, the action is canceled, but the signal is no longer
dropped so that the second character is properly inserted.
|
|
CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.
|
|
This allows to define on purpose the very same notation in different
files, as currently the notations for *, +, - in Nat.v and Peano.v
(with the first one using variables n and m and the second one using
the default variables used by Infix, namely x and y).
This makes also the "notation-overridden" warning less enigmatic
facing two notations which are the same up to the choice of names.
|
|
|
|
This assertion checked that two arguments in the same position were equal,
but in fact, since one might have already been reduced, they are only
convertible (which is too costly to check in an assertion).
|
|
Was PR#232: Fix the parsing of goal selectors.
|
|
|
|
The default value of the warnings flag was printed as an empty string,
now replaced by "default".
|
|
|
|
|
|
|
|
It seems we have no grammar rule that parses floats, so I'm
parsing an integer, but the whole machinery supports floats.
|
|
|
|
|
|
Importing VectorNotations breaks `; []`. So we make sure it's not
imported by defualt. Some files might be required to `Import
VectorDef.VectorNotations` rather than just `Import VectorNotations`.
|
|
Also delimit vector_scope with vector, so that people can write %vector
without having to delimit it themselves.
|
|
The no-inversion and maximal abstraction over dependencies now
supports abstraction over goal variables rather than only on "rel"
variables. In particular, it now works consistently using
"intro H; refine (match H with ... end)" or
"refine (fun H => match H with ... end)".
By doing so, we ensure that all three strategies are tried in all
situations where a return clause has to be inferred, even in the
context of a "refine".
See antepenultimate commit for discussion.
|
