| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fix the ordering of the results in the output of Search to correspond
to the "priority" ordering.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263.
String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
|
|
|
|
|
|
- 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.
|
