| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
A worker should never have to access the still-to-be-proved
obligations. If that happens, raise an informative anomaly.
|
| |
|
|
|
| |
This type contains a few unmarshallable fields, which can cause STM
workers to break in unpleasant ways when running queries
|
| |
|
|
|
|
|
|
|
|
|
| |
maybe ca71714).
Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.
was working in 8.4 but was failing in 8.5beta2.
Note: Changes in tacintern.ml are otherwise purely cosmetic.
|
| | |
|
| |
|
|
|
| |
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
| |
|
|
| |
I used a low-level function, now changed to `msg_notice`.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This mirrors the existing extraction libraries for OCaml.
One wart: the extraction for [string] requires that the Haskell code
imports Data.Bits and Data.Char. Coq has no way to add extra import
statements to the extracted code. So we have to rely on the user to
somehow import these libraries (e.g., using the -pgmF ghc option).
See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189
Message to github robot: this commit closes #65
|
| | |
|
| |
|
|
|
| |
Ideally, the code should be shared between the various toplevels, but this
is a lot more work than just fixing a few strings.
|
| | |
|
| | |
|
| |
|
|
| |
"Conjecture" (see #4252).
|
| |
|
|
|
| |
Was making the study of bugs like #4139 painful.
Now printing a better error message when a compiled file is missing.
|
| | |
|
| | |
|
| |
|
|
| |
Wrong handling of algebraic universes that have upper bounds.
|
| |
|
|
| |
Hence we reuse the ones in master.
|
| | |
|
| | |
|
| |
|
|
| |
with other reduction machines.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Patch provided by Çagdas Bozman.
|
| | |
|
| |
|
|
|
|
|
| |
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)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This makes the treatment of universe constraints/normalization more
understandable in the Sync/Async case:
- if one has to keep the constraints of the body and the type of
a lemma separate, then equations coming from the body are kept
(see: 866c41 )
- if they can be merge then the equations (substituted on both the
body and type) can be removed (one of the sides occurs nowhere)
The result is that, semantically, the constraints of a lemma do not
depend on weather it was produced asynchronously (v->vio->vo, or in
a CoqIDE session) or synchronously (v->vo).
Still the internal representation of the constraints changes to
accommodate an optimization (to reduce the size of the constraint set):
- in the synchronous case (some) equations are substituted (in both the
type and body), hence they can be completely dropped from the constraint
set
- in the asynchronous case (some) equations are substituted in the body
only (the type is fixed once and for all before the equations are
discovered/generated), hence these equations are necessary to relate
the type and the (optimized) body and are hence kept in the constraint
set
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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 grants wish #4194.
|
| |
|
|
| |
Thanks to Vadim Zaliva for testing.
|
| |
|
|
|
|
|
|
|
|
| |
Fixed #4241 correlates Printing Width and max_indent, this patch
changes the correlation to the following one:
max_indent = max ((wdth*80)/100) (wdth-30)
i.e. the right column defined by max_indent is 20% of the global
width, but capped to 30 characters.
|
| |
|
|
| |
when printing width extend).
|
| |
|
|
|
| |
found in the file system have the expected lowercase/uppercase
spelling)
|
| |
|
|
|
|
|
| |
Evars already had their own extensible state, but adding it globally allows
to write out extensible state-passing code in e.g. plugins. The additional
data is hopefully transparently preserved by the code out there. Trespassers
ought to be prosecuted.
|
Enrico Tassi
Alec Faithfull
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Arnaud Spiwack
Theo Zimmermann
Clément Pit--Claudel
Nickolai Zeldovich
Guillaume Melquiond
Cyprien Mangin
Matthieu Sozeau
Pierre Courtieu