| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
|
|
|
|
Reviewed-by: ppedrot
|
|
size. (Fixes #10956)
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: vbgl
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Ack-by: Blaisorblade
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: JasonGross
Ack-by: ppedrot
|
|
This should ideally have been done before the 8.11 branching.
|
|
Reviewed-by: ppedrot
|
|
- only one space instead of two when printing "{| |}"
- removing a redundant clause in the grammar of record_patterns
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
This means return_proof is the only place where it can be produced.
We need to change the stm a bit as it keeps a pointer to a
[closed_proof_output] to join and to check if it failed, and it needs
a way to create a dummy in 1 case.
I'm not sure if this works correctly though, how to test?
We also inline the used bits of [return_proof ~allow_partial:true] in
[save_lemma_admitted] to get [Proof using] info. We could
alternatively expose the [closed_proof_output -> constr list]
projection. I think the code is easier to understand this way though,
as we don't have to read [return_proof] and figure out that the side
effect manipulation is ignored etc.
Note that the "this will warn" comment was outdated since
73daf37ccc7a44cd29c9b67405111756c75cb26a
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
is fixed
Reviewed-by: Zimmi48
|
|
This should fix the issue when creating new session panes. The initial
session panes, however, might still be wrongly sized, as we do not yet
know, at the time they are created, if the window manager will respect the
user settings fixing the window size.
|
|
The bug was introduced by #10063, which eagerly added dots to identifier
without considering whether they are related to the identifier. Along the
way, this commit also prevents primes and digits from being added as
initial characters of identifiers. This works for both word selection and
queries.
Note that there is still a small issue with word selection, when the
current word starts with a digit. Indeed, when double-clicking, GTK will
already have extended the selection to it, so we have no way of preventing
the digit from being part of the selection.
This commit also fixes the unusual calling convention of
Gtk_parsing.end_words.
|
|
(by the checker refactor AFAICT)
+ fix commit for the coqtop side fix (it got rebased at some point)
Close #10705
|
|
a module
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
Reduction.whd_all does not commute with to_constr.
|
|
This probably does not work well in general, and specifically avoids
an anomaly fixing https://github.com/coq/coq/issues/10060
|
|
|
|
|
|
|
|
|
|
Close #10242
|
|
"dev" was not implied, and this can cause the following issues:
--8<---------------cut here---------------start------------->8---
$ docker run --rm -it coqorg/base:latest
coq@…:~$ opam update
coq@…:~$ git clone https://github.com/coq/coq.git
Cloning into 'coq'...
coq@…:~$ cd coq
coq@…:~/coq$ opam pin add -n -k path coq .
[coq.8.10.1] synchronised from file:///home/coq/coq
coq is now pinned to file:///home/coq/coq (version 8.10.1)
# issue 1. opam picks the first version he finds for coq from repos…
coq@…:~/coq$ mv coq.opam foo.opam
coq@…:~/coq$ opam pin add -n -k path foo .
Package foo does not exist, create as a NEW package? [Y/n] y
[foo.~dev] synchronised from file:///home/coq/coq
foo is now pinned to file:///home/coq/coq (version ~dev)
# issue 2. if none is found, opam sticks to some "~dev" version…
--8<---------------cut here---------------end--------------->8---
|
|
Reviewed-by: Zimmi48
|
|
@eelcovisser told me that the strategies in Luttik and Visser 97 were inspired
by Elan, but they are not part of Elan. They are part of the Stratego language.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
relation
Reviewed-by: gares
|
|
Now it uses `.. deprecated` like all the other deprecation notices in
the manual.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
|
|
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
