| Age | Commit message (Collapse) | Author |
|---|
|
|
|
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
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.
|
|
This commit is chiefly about moving code around to ease readability.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Correcting the code w.r.t. to the API was not the right solution. Instead,
the API comment had to be corrected.
|
|
We ensure statically by typing that the tags used by the rich printer
are integers. Furthermore, we also expose through typing that tags are
irrelevants in the returned XML.
|
|
|
|
|
|
Contrarily to what was described in the API, nodes without annotations
were not ignored by the printer but left there instead.
|
|
|
|
|
|
of syntax in test file ltac.v.
|
|
|
|
This is necessary for the patch for #4221 (817308ab5) to work.
|
