| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
- A few tweaks of string are now done via the Bytes module
- lots of String.capitalize_ascii and co
|
|
No more pp_alias_spec et pp_alias_decl.
Instead, we use "include" and "module type of".
The extracted code might hence need OCaml 3.12 (quite rarely)
|
|
Not_found)
This clarifies the execution flow
|
|
|
|
A double call to pp_module_type inside Ocaml.pp_specif was
causing an complexity blowup when pretty-printing heavily modular
extracted code.
I wasn't able to figure out why this double call is there. It could
be the leftover of some intermediate work in 2007 before commit 350398eae
(which introduced global printing phases Pre/Impl/Intf).
Anyway I'm reasonably sure that today these two pp_module_type calls produce
the exact same pretty-printed signature (even if there's a large bunch of
imperative states around). Moreover, this duplicated signature is actually
slightly wrong: when we alias a module M with a unambiguous name like Coq__123,
the type of Coq__123 should not be an exact copy of the type of M, but rather
a "strengthened" version of it (with equality between inductive types).
So the best solution is now to use this funny feature of OCaml introduced in 3.12 :
module Coq__123 : module type of struct include M end
This "module type of struct include" is slightly awkward, but short, correct,
and trivial to produce :-). And I doubt anybody will object to the (rare) use
of some 3.12 features in extracted code of 2017...
|
|
A double call to pp_module_type inside Ocaml.pp_specif was
causing an complexity blowup when pretty-printing heavily modular
extracted code.
I wasn't able to figure out why this double call is there. It could
be the leftover of some intermediate work in 2007 before commit 350398eae
(which introduced global printing phases Pre/Impl/Intf).
Anyway I'm reasonably sure that today these two pp_module_type calls produce
the exact same pretty-printed signature (even if there's a large bunch of
imperative states around). Moreover, this duplicated signature is actually
slightly wrong: when we alias a module M with a unambiguous name like Coq__123,
the type of Coq__123 should not be an exact copy of the type of M, but rather
a "strengthened" version of it (with equality between inductive types).
So the best solution is now to use this funny feature of OCaml introduced in 3.12 :
module Coq__123 : module type of struct include M end
This "module type of struct include" is slightly awkward, but short, correct,
and trivial to produce :-). And I doubt anybody will object to the (rare) use
of some 3.12 features in extracted code of 2017...
|
|
A double call to pp_module_type inside Ocaml.pp_specif was
causing an complexity blowup when pretty-printing heavily modular
extracted code.
I wasn't able to figure out why this double call is there. It could
be the leftover of some intermediate work in 2007 before commit 350398eae
(which introduced global printing phases Pre/Impl/Intf).
Anyway I'm reasonably sure that today these two pp_module_type calls produce
the exact same pretty-printed signature (even if there's a large bunch of
imperative states around). Moreover, this duplicated signature is actually
slightly wrong: when we alias a module M with a unambiguous name like Coq__123,
the type of Coq__123 should not be an exact copy of the type of M, but rather
a "strengthened" version of it (with equality between inductive types).
So the best solution is now to use this funny feature of OCaml introduced in 3.12 :
module Coq__123 : module type of struct include M end
This "module type of struct include" is slightly awkward, but short, correct,
and trivial to produce :-). And I doubt anybody will object to the (rare) use
of some 3.12 features in extracted code of 2017...
|
|
|
|
In particular, this closes bug 2417.
|
|
It will be possible to replace any call to 'autounfoldify x' with 'autounfold with x'.
|
|
The use case is to take a hint database as an argument of Ltac or Tactic Notation.
|
|
Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15
minutes which is too much for Travis. Pity, because it was a nice use case.
|
|
|
|
|
|
Types were a bit difficult to read as they were mostly based on
anonymous products, this commit replaces them by named records and
refactors out some imperative code.
There is still quite a bit of room for improvement, but at least the
records provide a basis for more fine-grained understanding and
documentation.
|
|
|
|
|
|
|
|
|
|
iris-coq math-classes sf
- [TLC] [metacoq] not ready for 8.6 yet
|
|
|
|
- Add README.ci
Suggestions and comments welcome.
- Use the system compiler to get some boot speedup.
- Build log folding.
- Set NJOBS=2 (very moderate speedup)
- Set language to a defined value.
OPAM itself recommends C, so we follow suit.
- Remove spurious `.opam`test
No harm in testing we are in the right opam setting even if the
cache did exist.
Anyways, it seems that the previous was spurious, as it was testing
if ~/coq/.opam did exists. I think the correct command would have
been:
```shell
[ -e ${HOME}/.opam ] || opam init ...
```
See the log at https://travis-ci.org/coq/coq/builds/198948812 for an
example.
|
|
- Improve the setup to support external contribs.
We use a more minimalistic Coq build, gaining a few extra minutes.
- [math-comp] workaround `make -j` bug to enable parallel building.
|
|
We also optimize `travis_wait` use.
|
|
|
|
lambda is self-quoting, see elisp manual, section 12.7 Anonymous
Functions
|
|
|
|
|
|
Commits were squashed.
|
|
|
|
|
|
|
|
|
|
This was introduced in 8.5 while reorganizing the structure of
intro-patterns.
|
|
- Do not use induction/elim when not necessary: use destruct or
destructive intro-pattern instead.
- Do not use heavy automation when lightweight automation is enough.
- Prefer shorter proofs when it does not hinder readability.
- Do not rely on automatically generated names.
- Use bullets.
|
|
|
|
|
|
|
|
The comment was arguing against the "Proof proof_term." syntax.
This syntax is still there 15 years later (while the alternative
proposition uses outdated syntax).
|
|
|
|
|
|
|
|
This is a modest contribution serving before all the purpose of
displaying the focus stack and the shelf and give_up list. It does not
print the sigma (while it could).
Any improvements are welcome.
|
|
The native compiler doesn't support `Require` inside `Module` sections
in some cases, we improve the error message. See:
https://coq.inria.fr/bugs/show_bug.cgi?id=4335
This patch improves the error message and gives the user some
feedback.
|
|
We complete the support of 'pat in this particular case (a 'pat under
a binder in a notation).
|
|
|
|
|
|
Tracking conversion problems to reconsider was lost for evars subject
to restriction (field last_mods was not updated and conversion
problems not considered to be changed).
|
