| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Bug #4957 was "unify cannot directly unify universes with evars, but can
do so indirectly".
|
|
|
|
|
|
This commit does not modify the signature of the involved modules, only
the opaque proof terms.
One has to wonder how proofs can bitrot so much that several occurrences
of "replace 4 with 4" start appearing.
|
|
|
|
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
|
|
|
|
For now we only normalize sorts, and we leave instances for the next
commit.
|
|
|
|
The kernel does fishy things with casts, such that ensuring there are no
two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr
view as well.
|
|
This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance
difference was not conclusive enough to pay for the code ugliness.
|
|
We do one step of loop unrolling, limit the number of allocations and
mark the function as inline.
|
|
|
|
|
|
|
|
|
|
Added a function that takes the first [p] elements of a vector, and
a few lemmas proving some of its properties.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This broke the build of iris-coq in the EConstr branch. Each time you
use unsafe_type_of, I loose a night of sleep, so please stop.
|
|
|
|
|
|
Was breaking e.g. fiat-crypto.
|
|
This is while waiting for a possible different solution, if ever such
a different solution is adopted, since the coq.inria.fr/library has
currently a broken link and someone rightly complained about it.
|
|
|
|
To handle dynamic printing in CoqIDE we listen to the
`size_allocate` signal , [see more details in
6885a398229918865378ea24f07d93d2bcdd2802]
However, we must be careful to protect against scrollbar creation: it
is possible for the `size_allocate` handler to change the size when
inserting text (due to scrollbars), thus we may enter in an infinite
loop.
Our fix is to check if the width has really changed, as done in
`Wg_MessageView`.
This fixes the problem noted by @herbelin in
https://coq.inria.fr/bugs/show_bug.cgi?id=5417
|
|
|
|
We don't need to look for the size of the whole list to find whether we can
extract a suffix from it, as we can do it in one go instead. This slowness
was observable in abstract-heavy code.
|
|
This turned out to be costly in proofs with many abstracted lemmas, as an
important part of the time was passed in the computation of the size of the
opaquetab.
|
|
In one case, the hashconsed type of a judgement was not used anywhere else.
In another case, the Opaqueproof module was rehashconsing terms that had
already gone through a hashconsing phase. Indeed, most OpaqueDef constructor
applications actually called it beforehand, so that the one performed in
Opaqueproof was most often useless. The only case where this was not true
was at section closing time, so that we tweak the Cooking.cook_constant to
perform hashconsing for us.
|
|
|
|
After 5db9588098f9f, some extra evar-normalization remained (compared to trunk)
that would change the semantics e.g. of change bindings under Ltac match.
This is just circumventing a fundamental flaw in the treatment of patterns.
|
|
|
|
|
|
|
|
This is the good parts of PR #360.
IIUC, these vernacular were meant mostly for debugging and they are
not supposed to be of any use these days.
Back and join are still there not to break the testing infrastructure,
but some day they should go away.
|
|
|
|
|
|
Also adding spaces around ":=" and ":" when printed as "(x : t := c)".
Example:
Check fun y => let x : True := I in fun z => z+y=0.
(* λ (y : nat) (x : True := I) (z : nat), z + y = 0
: nat → nat → Prop *)
|
|
|
|
|
|
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
|
