| Age | Commit message (Collapse) | Author |
|---|
|
We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
|
|
This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.
Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.
|
|
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
|
|
This reverts commit 9f4e67a7c9f22ca853e76f4837a276a6111bf159.
|
|
|
|
assumed.
|
|
So that fixpoints and cofixpoints which are assumed to be total are highlighted in yellow in Coqide, for instance.
|
|
The `search_guard` function is called to infer the recursive argument of fixpoints. For each potential argument, it tests whether it is called structurally, calling the kernel test. When a single argument is available either because `{struct x}` was specified, or because there is a single inductive argument, the kernel test is performed, despite the fact that the kernel will do it later, and the kernel error reraised. It is unnecessary.
|
|
The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
|
|
The syntax is `Fixpoint Assume[Guarded] …`. For some reason `Assume [Guarded] Fixpoint` broke the parser.
|
|
|
|
guardedness.
|
|
|
|
|
|
|
|
They appear as axioms of the form `Foo is positive`.
|
|
the interfaces.
|
|
The syntax is `Assume [Positive]` Inductive/CoInductive/Record…`. The square brackets are used to delimit what is actually a list, so that other such flags can be passed in the future (universes, guard condition…).
|
|
Makes sure not to generate inductive schemes of assumed positive types.
|
|
The request for positivity to be assumed is honored.
|
|
The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.
|
|
positivity is assumed.
|
|
I wasn't very creative: I just added a single test by failure case in the positivity checker (plus one success).
There should probably be tests with mutually inductives and co-inductives as well.
|
|
|
|
Fixes bug 3936
This closes #73
|
|
|
|
This interface is promoted by the operf-macro tool
https://github.com/OCamlPro/operf-macro
which allows to run benchmarks of time and memory usage
of various OCaml programs.
Coq already has two ways to get Gc infos:
- the -m|--memory command-line flag prints the total heap words allocated
- the "Print Debug Gc" command prints much more information,
but in a Coq-implementation-defined format that is not suitable
for across-programs comparison
(also an environment variable allows to profile Coq runs on any .v,
in an non-intrusive way)
Note to the Github Robot:
This closes #75
|
|
Marshalled libraries are only loaded when needed and dropped thereafter.
This might be costly for Require inside modules, but such a practice is
discouraged anyway.
|
|
The first part only contains the summary of the library, while the second
one contains the effective content of it.
|
|
A worker should never have to access the still-to-be-proved
obligations. If that happens, raise an informative anomaly.
|
|
This type contains a few unmarshallable fields, which can cause STM
workers to break in unpleasant ways when running queries
|
|
maybe ca71714).
Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.
was working in 8.4 but was failing in 8.5beta2.
Note: Changes in tacintern.ml are otherwise purely cosmetic.
|
|
|
|
|
|
This allows fatal_error to be used for printing anomalies at loading time.
|
|
Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.
|
|
I used a low-level function, now changed to `msg_notice`.
|
|
|
|
|
|
|
|
|
|
|
|
This is my attempt at understanding each case and subfunction of the positivity check and document each of them to the best of my capacity.
|
|
|
|
Message to the github robot:
This closes #63
|
|
|
|
Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show
Intros] at the end of a proof:
Goal True. trivial. Show Intros.
|
|
This mirrors the existing extraction libraries for OCaml.
One wart: the extraction for [string] requires that the Haskell code
imports Data.Bits and Data.Char. Coq has no way to add extra import
statements to the extracted code. So we have to rely on the user to
somehow import these libraries (e.g., using the -pgmF ghc option).
See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189
Message to github robot: this commit closes #65
|
|
|
|
|
