| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
Reviewed-by: fajb
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: mattam82
|
|
|
|
|
|
|
|
|
|
#10239).
The bug was introduced in #10239 which seems to have actually remained
half-done: "wit_intropattern" and "wit_simple_intropattern" did not
share the same representation of values (val_tag) but the code was
assuming (especially the code for "fresh") that this was shared.
We fix it by sharing the internal representation (`dyn` field in
Tacarg.make0) as suggested by @ppedrot in the discussion of #10239
(this allows also to simplify Taccoerce.is_intro_pattern).
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Failing CI is BAD. #10476 should not have been merged without a
solution for SF being found, or the test being marked temporarily as
allow failure.
|
|
On tags, the pkg:nix:deploy:channel job was run even though the
required pkg:nix:deploy was not. We repeat the same conditions
regarding refs as in pkg:nix:deploy. Cf. GitLab's doc on the meaning
of several only conditions:
https://docs.gitlab.com/ee/ci/yaml/README.html#onlyexcept-advanced
|
|
|
|
It will take non-trivial effort to make Coq work with OCaml >= 4.10.0.
|
|
|
|
This was broken by change 6608f64.
|
|
|
|
We allow the build to use some deprecated primitives in OCaml
4.09.0, for more details see bug #10602
|
|
Now that we place imperative module declaration on top of module
interpretation we can remove the abstraction layer used in
`Declaremods`, so the `interp_modast` parameter goes away.
Improvement suggested by Gaëtan Gilbert.
|
|
We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.
This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.
The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.
This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot
Ack-by: vbgl
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
This helps extraction by not building sigT which can lower to Prop by
template polymorphism.
Bug #10757 can probably still be triggered by using module functors to
hide that we're using Prop from Program Fixpoint but that's probably
unfixable without fixing extraction vs template polymorphism in
general.
In passing we notice that Program doesn't know how to telescope SProp
arguments, we would need a bunch of variants of sigma types to deal
with it (or use Box?) so let's figure it out some other time.
We also reuse the universe instance to avoid generating a bunch of
short-lived universes in the universe polymorphic case.
|
|
Prove that morphisms preserve additions
Fix stdlib index
Prove that constructive real morphisms preserve multiplications by integers
Prove that constructive real morphisms preserve multiplications by rationals
Prove CReal_mult_pos_appart_zero
Prove that constructive real morphisms preserve multiplications
Prove that constructive real morphisms preserve divisions
Rewrite convergence in sort Prop, to extract smaller programs
Rewrite convergence on integers, to extract smaller programs
Fix typos
|
|
The logic is implemented in OCaml. By induction over the terms,
guided by registered Coq terms in ZifyInst.v, it generates a rewriting
lemma. The rewriting is only performed if there is some progress. If
the rewriting fails (due to dependencies), a novel hypothesis is
generated.
This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848
ans fixes #10755.
The zify plugin is placed in the micromega directory.
(Though the reason is unclear, having it in a separate directory is
bad for efficiency.) efficiency impact.
There are also a few improvements of lia/lra that are piggybacked.
- more aggressive pruning of useless hypotheses
- slightly optimised conjunctive normal form
- applies exfalso if conclusion is not in Prop
- removal of Timeout in test-suite
|
|
|
|
|
|
|
|
|
|
This should compensate the removal of the library-level optimization,
while maintaining correct behavior.
|
|
They have been already cached at loading time.
|
|
`Import` does not actually need to register an object, only `Export`
does. So we specialize and rename the object into `ExportObject`.
|
|
|
|
Libraries are now handled like other modules.
|
|
CoqIDE windows not always set at the expected position
Reviewed-by: ppedrot
Reviewed-by: silene
|
|
G. Melquiond noticed that the size_allocate event is emitted in the
Layout step of the Events-Update-Layout-Paint gtk+ loop so that it is
actually processed only when a further event arrived. In some
circonstances, this next event has to be an action from the user. So,
in some circonstances, at initialization of Coqide, the handle, whose
positioning was precisely governed by the size_allocate event, was
only set at its expected position after a first action of the
user. Before this first action of the user, the handle separating the
buffer and the pair of goal and message windows, as well as the handle
separating the goal window and the message window were located in the
leftmost uppermost corner, which gave an impression of non-usability
of CoqIDE.
To prevent this, we early set the position of the handle at an
estimated value depending on the width and height of the whole coqide
windows in the preferences.
(Also removing a previous temporary setting of the handle position to
- strangely - value 1 but this was anyway overwritten by the
size_allocate event.)
|
|
Reviewed-by: cpitclaudel
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: ppedrot
|
|
E.g., if one wish to instantiate these evars manually, in another way
than with reflexivity.
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
|
