| Age | Commit message (Collapse) | Author |
|---|
|
We add a fast path when generalizing over variables.
|
|
Ack-by: Zimmi48
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: ejgallego
|
|
|
|
The OPAM build has been broken it seems since almost the beginning as
OPAM doesn't substitute variables in the almost undocumented
`build-env` form.
Packages built this way worked as Coq used a different method to
locate `coqlib`, however the value for `coqlib` was incorrect.
We set instead the right prefix using an explicit configure call.
|
|
We also update the plugin tutorial.
This was already tried [in the same exact way] in #8811, however the
bench time was not convincing then, but now things seem a bit better,
likely due to the removal of some extra normalization somewhere.
Some more changes from #8811 are still pending.
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Currently this env is only used to error for Printing If/Let on
non-2-constructor/non-1-constructor types so we could alternatively
remove it and not error / error later when trying to print.
Keeping the env and the error as-is should be fine though.
|
|
This was introduced by @herbelin in
817308ab59daa40bef09838cfc3d810863de0e46, appears to have been
made unnecessary again by herbelin in
4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6.
At this point it appears to be completely unused.
|
|
|
|
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
|
|
|
|
|
|
PR #8187 misplaced its CHANGES entry. We remove it in this commit instead
of moving it to the right place because it is reverted in #9987.
|
|
|
|
|
|
Add more links to PRs and credits of authors.
|
|
|
|
|
|
Mainly markup fixes by Theo
Co-Authored-By: mattam82 <matthieu.sozeau@inria.fr>
|
|
|
|
ProofGeneral (master branch)
Reviewed-by: ejgallego
|
|
`nonPropType` interface
Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ggonthier
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: maximedenes
|
|
** 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.
|
|
|
|
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
|
