| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
Message to the github robot:
This closes #63
|
| | |
|
| |
|
|
|
|
|
| |
Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show
Intros] at the end of a proof:
Goal True. trivial. Show Intros.
|
| | |
|
| |
|
|
|
|
|
| |
Of course there is an exception to the previous commit.
Fail used to print even if silenced but loading a vernac file.
This behavior is useful only in tests, hence this flag.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trying to untangle the flags:
coqc -verbose coqtop -compile-verbose are used just to print the commands run;
-quiet, -silent, Set Silent, Unset Silent control Flags.verbose flag.
Flags.verbose controls many prints that are expected to be made in
interactive mode. E.g. "Proof" or "tac" prints goals if such flag is
true. To flip it, one can "Set/Unset Silent" in both coqtop and coqc
mode.
It is still messy, but the confusion between -verbose and Flags.verbose
has gone (I must have identified the two things with my initial STM
patch)
|
| |
|
|
|
|
| |
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
| | |
|
| | |
|
| |
|
|
|
| |
This disables colors in emacs compilation buffer, which does not
support ansi colors by default.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
For now, warnings are still ignored by default, but this may change. This
commit at least allows to print them whenever desired. The -w syntax is
also opened to future additions to further control the display of
warnings.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
| | |
|
| |
|
|
|
|
|
| |
In compiler mode, only vernac.ml knows the current file name.
Stm.process_error_hook moved from Vernacentries to Vernac to
be bale to properly enrich the exception with the current file
name (if any).
|
| | |
|
| |
|
|
|
|
|
| |
The command [Redirect "filename" (...)] redirects all the output of
[(...)] to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
|
| | |
|
| |
|
|
|
|
| |
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
| | |
|
| |
|
|
|
|
| |
This patch should get rid of the following warning:
Invalid character '-' in identifier "v8-syntax".
|
| |
|
|
|
|
|
|
|
|
| |
The solution is a bit ugly. In order for two tactic notations identifiers not
to be confused by the inclusion from two distinct modules, we embed the name of
the source module in the identifiers. This may still fail if the same module is
included twice with two distinct parameters, but this should not be possible
thanks to the fact any definition in there will forbid the inclusion, for it
would be repeated. People including twice the same empty module otherwise
probably deserve whatever will arise from it.
|
| |
|
|
| |
definition time. The obligation tactic or user can still choose to do so.
|
| |
|
|
| |
instances as definitions and lemmas do (fixes bug# 4121).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
subdirectories.
Using Mltop.add_path instead of Mltop.add_rec_path causes the following
kind of behavior:
$ coqtop -nois
Coq < Require Import Coq.Init.Datatypes.
Error: Cannot find a physical path bound to logical path Coq.Init.
The only case where its use is still warranted is the implicit "." path. It
shall not be recursive because Coq might be called from about anywhere.
This patch also removes -I-as since its behavior is no longer the one from
8.4 so it is not worth keeping it around.
|
| |
|
|
|
| |
"Add LoadPath" is documented as acting as -Q, not as -I-as. Note that
"Add Rec LoadPath" should be used when compatibility with 8.4 matters.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This reverts commit 124734fd2c523909802d095abb37350519856864.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
This commit also removes the extraneous "=>" token from Fail messages and
prevents them from losing all the formatting information.
|
| | |
|
| |
|
|
|
|
|
| |
Instead of substituting carelessly the recursive names in Ltac interpretation,
we declare them in the environment beforehand, so that they get globalized
as themselves. We restore the environment afterwards by transactifying the
globalization procedure.
|
| |
|
|
| |
Fixes bug #4089.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Although these commands were never deprecated, they have been unusable for some
time now, since they send requests to an Italian server which is no longer
alive.
|
| |
|
|
| |
goal in Instance. Also remove some dead code.
|
| |
|
|
| |
Of course such proofs cannot be processed asynchronously
|
| |
|
|
| |
Fixes #3809.
|
Pierre-Marie Pédrot
Clément Pit--Claudel
Enrico Tassi
Matthieu Sozeau
Pierre Courtieu
Guillaume Melquiond
Hugo Herbelin
Matthieu Sozeau
Daniel R. Grayson
Maxime Dénès