| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
No need to keep track of it this way now that this data is part of the
kernel.
|
|
This allows to remove the double declaration of monomorphic universes of
discharged section constants. This also makes it much clearer that only
the first declaration of a constant is allowed to declare delayed
constraints.
As a nice bonus, this simplifies the Opaqueproof API.
|
|
This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
|
|
|
|
Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.
|
|
This is not quite pretty, but it is needed by the section mechanism to rebuild
an inductive when closing a section. Hopefully this can be moved back at some
point.
|
|
For now we only keep a count of the number of open sections, discriminating
between polymorphic and monomorphic ones.
|
|
The section local universes are undoubtedly ordered, but the API was requiring
an unordered ContextSet. We also move the naming one level up.
Unfortunately, some callers are currently defining the same polymorphic
universes in a section several times, notably the "Variable" command. I had
to hack around this behaviour.
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
|
|
intropattern entry in #10239)
Reviewed-by: ppedrot
|
|
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
|
|
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
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
