| Age | Commit message (Collapse) | Author |
|---|
|
|
|
shortening a strict prefix of an application
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
|
|
|
|
Reviewed-by: maximedenes
|
|
|
|
Z.to_euclidean_division_equations
|
|
This reverts commit b49f4e966443a76ac70d37c4cde68f94de164c01.
It turns out the 4x was due to .nia.cache (because I didn't clean
sufficiently in testing), not due to `subst`.
|
|
This speeds up the file from 2m32s to
```
real 0m41.851s
user 0m41.512s
sys 0m0.376s
```
Also note the `subst` trick in the doc.
|
|
Also fold it into `Z.div_mod_to_quot_rem`
Note that the test-suite file is a bit slow. On my machine, it is
```
real 2m32.983s
user 2m32.544s
sys 0m0.492s
```
|
|
Note that we define a `cleanup` tactic which is essential for speed of
reasoning. Perhaps this tactic should make it into the code for
`Z.div_mod_to_quot_rem` somewhere?
```coq
Ltac cleanup :=
repeat match goal with
| [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
| [ H : ?T -> _, H' : ~?T |- _ ] => clear H
| [ H : ~?T -> _, H' : ?T |- _ ] => clear H
| [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
| [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
| _ => progress subst
end.
```
|
|
Alas, I have not had time to work on imrpoving the performance of nia,
and there has been a request to include this tactic (which is useful on
its own) without bundling it into `zify`. So that is what we do here.
I leave the definition of it in `PreOmega` in case we want to eventually
include it in `zify`/`nia`.
|
|
The various (micr)omega tactics now support `Z.div` and `Z.modulo`.
I briefly looked into supporting `Nat.div` and `Nat.modulo`, but the
conversions between `Z.div` and `Nat.div` are defined in `ZArith.Zdiv`,
which depends on `Omega`, which depends on `PreOmega`, which is where
`zify` is defined.
|
|
This commit was created via `./dev/tools/update-compat.py --master`
|
|
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: mattam82
Ack-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
computed
Reviewed-by: ejgallego
|
|
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
|
|
Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
|
|
Using a unit test as it's way faster than messing with universes.
You can test with universes by
~~~coq
Set Universe Polymorphism.
Definition x1@{i} := True.
Definition x2 := x1 -> x1.
Definition x3 := x2 -> x2.
Definition x4 := x3 -> x3.
Definition x5 := x4 -> x4.
Definition x6 := x5 -> x5.
Definition x7 := x6 -> x6.
Definition x8 := x7 -> x7.
Definition x9 := x8 -> x8.
Definition x10 := x9 -> x9.
Definition x11 := x10 -> x10.
Definition x12 := x11 -> x11.
Definition x13 := x12 -> x12.
Definition x14 := x13 -> x13.
Definition x15 := x14 -> x14.
Definition x16 := x15 -> x15.
Definition x17 := x16 -> x16.
Definition x18 := x17 -> x17.
Definition x19 := x18 -> x18.
About x19. (* 262144 universes *)
~~~
Note on my machine `About x18.` did not overflow even before this
commit.
|
|
|
|
|
|
This makes code paths clearer (we still factorize a lot of the
treatment), and we seize the opportunity to forbid anonymous
`Declare Instance` which is not a documented construction, and seems to
make little sense in practice.
|
|
|
|
|
|
This is for consistency with "rewrite {x..} y"
|
|
|
|
|
|
The code to generate the legacy bodies is moved to its only user in
extraction.
It almost seems like we could remove it (ie no special extraction code
for primitive projection constants) but then we run into issues with
automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets
extracted to `type foo = nat` and (if we remove the special code) `let
a = a`.
|
|
[About] still says it.
Close #9056.
|
|
|
|
Scripting these commands in async mode does not really make sense.
|
|
|
|
proofs.
We forbid commands that may open proofs inside proofs.
|
|
of the "in" clause of a "match"
|
|
|
|
This is a reworking of 7fd28dc9: instead of using words such as
"domain of", "codomain of" to refer to a position in the instance of
the original evar, we simply display the instance and the name of the
unresolved evar in this instance. This is both simpler and more
informative. (The positional words remain useful for printing the
evar_map in debugging though.)
In passing, this fixes #8369 (Not_found in printing message about an
unresolved subevar).
Incidentally add possible breaking while printing "in environment".
|
|
|
|
- The head of "in" was wrongly considered binding
- Aliases in the "in" pattern were not taken into account
|
|
This is slightly blunt, it might be the case that we get delayed constraints
that cannot be solved resulting in a later universe inconsistency, but it looks
highly unlikely on arithmetical statements.
Alternatively we would have threaded the unification state, but this would
have required a much deeper change.
Fixes #9268.
|
|
|
|
Thanks to Georges Gonthier for noticing it.
Expanding a few Pervasives.compare at this occasion.
|
|
|
|
|
|
|
|
|
|
Diff code uses the lexer to recognize tokens in the inputs, which can be
Pp.t's or strings. To add the highlights in the Pp.t, the diff code
matches characters in the input to characters in the tokens. Current
code fails for inputs containing quote marks or "(*" because the quote
marks and comments don't appear in the tokens. This commit adds a "diff
mode" to the lexer to return those characters, making the diff routine
more robust.
|
|
|
|
|
