| Age | Commit message (Collapse) | Author |
|---|
|
More precisely, GTK+ uses Pango rules which follows the standard Unicode
text segmentation rules (see http://www.unicode.org/reports/tr29/).
|
|
|
|
In practice, most of Alt modified keys are used on MacOS X keyboards
for special characters and many Command modified keys are used for
MacOS standard actions.
So, we propose to use Ctrl-Command- as a prefix for the Meta-based
nano-PG shortcuts. E.g. Ctrl-Command-e would go the end of the
sentence.
|
|
Not only will this be clearer but it prepares to describing action on
MacOS which shall use Cmd and which cannot be abbreviated w/o
introducing a confusion with the abbreviation C- of Control-.
|
|
For instance, Ctrl-Meta-e was behaving like Ctrl-e.
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: maximedenes
|
|
Backport
https://github.com/ocaml/ocaml/commit/71b94fa3e8d73c40e298409fa5fd6501383d38a6
and
https://github.com/ocaml/ocaml/commit/d3e86fdfcc8f40a99380303f16f9b782233e047e
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/c6ce97fe26e149d43ee2cf71ca821a4592ce1785
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/eb1922c6ab88e832e39ba3972fab619081061928
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/055d5c0379e42b4f561cb1fc5159659d8e9a7b6f
from OCaml VM
|
|
Backport
https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376
from OCaml VM
|
|
** Changed definition of `simpl_rel` to `T -> `simpl_pred T`, so that
`inE` will now expand `a \in r b`, when `r := [rel x y | R]` to `R{b/x,
a/y}`, as the expanding coercion is now only inserted in the _last_
application.
The old definition made it possible to have a `simpl_rel >-> rel`
coercion that does not block expansion, but this can now be achieved
more economically with the `Arguments … /.` annotation.
** Deleted the `[rel of P]` notation which is no longer needed with
the new `simpl_rel` definition, and was broken anyway.
** Added `relpre f R` definition of functional preimage of a notation.
** `comp` and `idfun` are now proper definitions, using the `Arguments
… /.` annotation to specify simplification on application.
** Added `{pred T}` syntax for the alias of `pred T` in the `pred_sort`
coercion class; deleted the `pred_class` alias: one should either
use `pred_sort` in `Coercion` declarations, or `{pred T}` in type casts.
Used `{pred T}` as appropriate in localised predicate (`{in …, …}`) theory.
Extended and corrected `pred` coercion internal documentation.
** Simplified the `predType` structure by removing the redundant
explicit `mem_pred` subfield, and replacing it with an interlocked
projection; deleted `mkPredType`, now replaced by `PredType`.
** Added (and extensively documented) a `nonPropType` interface
matching types that do _not_ have sort `Prop`, and used it to remove
the non-standard maximal implicits annotation on `Some_inj` introduced
in #6911 by @anton-trumov; included `test-suite` entry for `nonPropType`.
** Documented the design of the four structures used to control the
matching of `inE` and related predicate rewriting lemmas; added `test-suite`
entry covering the `pred` rewriting control idioms.
** Used `only printing` annotations to get rid of token concatenation
hacks.
** Fixed boolean and general `if b return t then …` notation so that
`b` is bound in `t`. This is a minor source of incompatibility for
misuses of this syntax when `b` is _not_ bound in `t`, and `(if b then
…) : t` should have been used instead.
** Reserved all `ssreflect`, `ssrfun` and `ssrbool` notation at the top
of the file, adding some printing boxes, and removing some spurious
`[pred .. => ..]` reserved notation.
** Fixed parsing precedence and format of `<hidden n>` notation, and
declared and put it in an explicit `ssr_scope`.
** Used module-and-functor idiom to ensure that the `simpl_pred T >-
pred T` _and_ `simpl_pred T >-> {pred T}` coercions are realised by the
_same_ Gallina constant.
** Updated `CREDITS`.
The policy implied by this PR: that `{pred T}` should systematically
be used as the generic collective predicate type, was implemented in MathComp
math-comp/math-comp#237. As a result `simpl_pred >-> pred_sort` coercions
became more frequent, as it turned out they were not, as incorrectly stated
in `ssrbool` internal comments, impossible: while the `simplPredType`
canonical instance does solve all `simpl_pred T =~= pred_sort ?pT`
instances, it does _not_ solve `simpl_pred T =~= {pred T}`, and so the
coercion will be used in that case. However it appeared that having two
different coercion constants confused the SSReflect keyed matching
heuristic, hence the fix introduced here. This has entailed some
rearrangement of `ssrbool`: the large `Predicates` section had to be
broken up as the module-functor idiom for aliasing coercions cannot be
used inside a section.
|
|
This arose after a question by Talia Ringer on how to log
user-interaction with a Coq document.
The hooks would allow a plugin to receive events about user data.
This is experimental and will need some tweaks to be useful for sure,
in particular w.r.t. errors.
[Note: this is safe enough as to be included in 8.9]
|
|
|
|
Reviewed-by: gares
Ack-by: herbelin
|
|
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
|
|
I ran `git shortlog -nse | sed s'/^[ 0-9\t]*//g' | sort | less` and
manually inspected the result for duplicates.
Then I used
```bash
git shortlog -nse | sed s'/^[ 0-9\t]*//g' | sort | sed s'/<.*>//g' | uniq -c | grep -v '^ *1 '
```
to check that there were no remaining duplicates.
|
|
Reviewed-by: maximedenes
|
|
as a hook
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
|
|
|
|
Closes #8410 (adapted from fix by @silene in the 8.9 branch)
|
|
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: erikmd
Ack-by: gares
Ack-by: jfehrle
|
|
not to be used.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
|
|
Reviewed-by: ppedrot
|
|
Ack-by: Zimmi48
Reviewed-by: maximedenes
Ack-by: proux01
Reviewed-by: vbgl
|
|
Reviewed-by: ppedrot
|
|
trigger a warning on MacOS X (and other BSD systems).
Ack-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: vbgl
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: gares
|
|
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
We have some discrepancy with the package names for plugins in the
META / Dune case. This PR fixes it.
At some point there was a need for plugin package names having to be
named as their directories.
I think this is not true anymore, but taking the "dir_name ==
package_name" convention just in case.
|
|
branch)
Adds XML-like tags in output to mark diffs
|
|
I believe this is the appropriate place for users to read about this, even tho
`unshelve` is technically a tactical.
This example was explicitly requested in #3225 and is commonly used in both
Iris (and was documented in the changelog at the time).
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
|
|
|
|
|
|
There is no more uses of "old style preferences" but the comment was
still there.
|
|
This avoids the modifiers keys to overwrite changes made in
coqide.keys.
|
|
|
