| Age | Commit message (Collapse) | Author |
|---|
|
Hurkens.v by dropping the artificial need for monad laws. Tactic eauto
decided to be dependent on the laws but there is a shorter proof
without them.
[Interestingly, eauto is not able to find the short proof. This is a
situation of the form
subgoal 1: H : ?A |- P x
subgoal 2: H : M ?A |- M (forall x, P x)
where addressing the second subgoal would find the right instance of
?A, but this instance is too hard to find by addressing first the
first subgoal.]
|
|
|
|
|
|
|
|
This is required since we merged PR#309: Ltac as a plugin.
|
|
|
|
This is in preparation for landing of PR#309: Ltac as a plugin
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
|
|
|
|
|
[travis] Add math-comp overlays, update CompCert to official version, add UniMath
|
|
|
|
We make math-comp overlays easier, we also start structuring the
scripts a bit more.
|
|
|
|
|
|
|
|
We extend `Stm.vernac_interp` so it can handle the commands it should
by level. This reenables `Show Script` handling, and this
interpretation function should handle more commands in the future such
as Load.
However note that we must first refactor the parsing state handling a
bit and remove the legacy `Stm.interp` before that.
|
|
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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...
|
|
|
|
Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15
minutes which is too much for Travis. Pity, because it was a nice use case.
|
