| Age | Commit message (Collapse) | Author |
|---|
|
(Fix bug #4348)
|
|
If it was intentional, please commit again separately.
|
|
The theories/ directory contains no cmi/cmxs files when native_compute is
disabled, so do not try to ship them.
|
|
of temporary hypotheses than 76f27140e6e34 did.
|
|
|
|
Native_compute is not working properly on Windows due to command line size
limitations and the lack of namespaces in OCaml. Using compiler-libs could
solve this, but it is unclear how to ensure stability w.r.t. future versions of
OCaml.
|
|
|
|
of "apply ... in ... as ..." in the context.
Fixing a regression done by 7e00e8d60 and f2130a88e1: when an evar is
created, the statement of the refined hypothesis virtually depends on
the whole context and has to be left at the top.
|
|
|
|
#4268)
|
|
|
|
|
|
This was because the traversal algorithm used canonical names instead of user
names, confusing which term was defined and which term was an axiom.
|
|
|
|
... 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.
|
|
|
|
|
|
|
