| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
| |
| |
| |
| | |
When reifying a 31-bit integer after a VM computation, we check that no bit
outside the 31 LSB is set to 1.
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
out to me by Pierre B.
Also extending use of bullets in Vectors where relevant.
|
| | |
| |
| |
| |
| | |
ago) which broke compilation of theories/Logic/WKL.v (collision
between a temporary name and a user name).
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
an initial hypothesis hyp at the same position in the context.
Ensuring the same for "apply c in hyp as pat".
Ensuring that "pose proof (H ...) as H" does not change the position of H.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
compatibility with the non uniform behavior that "intros [] []" on
"A*B->C*D->E" automatically introduces A and B but leaves C and D in
the goal.
Kept unset in 8.5 but planned to be set in 8.6.
|
| | | |
|
| | |
| |
| |
| | |
to behave like "specialize (H ...)" since 4/8/2008 (r11300, 7d515acbc5).
|
| | |
| |
| |
| | |
This (at least technically) solves the issue #4113 (see also #4329).
|
| | | |
|
| | |
| |
| |
| | |
clause in pattern-matching or not.
|
| | | |
|
| | |
| |
| |
| |
| | |
This allows to reduce the dependencies of subproofs generated by any sequence
of tactics. Grants wish #4327.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
Let-bindings were not taken into account, resulting in proof-terms way too
huge.
|
| |\| |
|
| | |
| |
| |
| | |
Previously, the kernel would silently fall back to standard conversion.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
On 64 bits architectures, integers could have some of their 32 msb set to 1
internally in the VM. When read back to a Coq term, this was not observable. But
an equality test would fail. From the user point of view, the symptom was that
vm_compute; reflexivity would succeed but the subsequent Qed would fail.
Bug reported by Tahina Ramananandro.
|
| | |
| |
| |
| | |
ADDMULDIVINT31 was missing pops in some cases
|
| |\| |
|
| | |
| |
| |
| |
| | |
The target creation process should eventually be automated, because it
is tedious and error-prone as witnessed by this commit.
|
| | |
| |
| |
| | |
"Fetching opaque proofs" notices are not printed by default anymore.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
The previous extraction of [Z.div] for Haskell did not properly handle
divide-by-zero. Fix it by introducing an explicit [if] statement in the
generated Haskell code.
Also, introduce a similar extraction rule for [Z.modulo], with the same
check for modulo-by-zero.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
The previous extraction of [Nat.div] for Haskell did not properly handle
divide-by-zero. Fix it by introducing an explicit [if] statement in the
generated Haskell code.
Also, introduce a similar extraction rule for [Nat.modulo], with the same
check for modulo-by-zero.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Hugo Herbelin proposed to modify directly the function
"check_correct_par" to simplify commit c12b430
(see the pullrequest's discussion).
Note that the constructor "LocalNonPar" has now three arguments (instead
of two). In LocalNonPar (n,i,l) n denotes the position among real
arguments (ie. ignoring letins), i is the rel index of the expecting argument
in the context of parameters and l is the index of the inductive.
|
| | | |
|
| | |
| |
| |
| |
| | |
I do not think that this information is worth displaying without
the verbose flag.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d
were generated by a call to coqdep using the argument -c (for ocaml
code). While doing some finetuning of the generation of implicit rules,
this commit removed (I think by mistake) this "-c". And without this
-c argument coqdep output nothing on mllib files leading to incorrect
linking of mllibs.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In PIDE based UIs queries can be delegated too, hence to speed up
things I was saving a shallow state. Unfortunately a shallow state
breaks section/modules commands, and a query can be the last entry
of a section/module. (A shallow state does essentially drop the libstack).
The easy solution is to save a complete state.
A better one would be to refine the static analysis of the document and
decide which kind of saved state one needs.
|
| | |
| |
| |
| |
| | |
There is no remaining hook in the preferences. In particular, the
refresh_editor_hook is gone.
|
| | | |
|
| | |
| |
| |
| | |
(48d611ff2a).
|
| | |
| |
| |
| |
| | |
There is no remaining global preference record anymore, every preference
is now defined in the new event-based style.
|
| | |
| |
| |
| | |
This commit is chiefly about moving code around to ease readability.
|
| | | |
|
| | |
| |
| |
| | |
Grants wish #2098.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
I don't know what was the intent of Pierre B here. In 8.4, it was not
supported, raising with an error at parsing time. I changed the
anomaly into an error at interpretation time, so it is still not
supported but we could support it if some legitimate use of it
eventually appears.
|
| | | |
|
| | | |
|
| | | |
|
Maxime Dénès
Pierre-Marie Pédrot
Hugo Herbelin
Catalin Hritcu
Gregory Malecha
Nickolai Zeldovich
mlasson
Enrico Tassi