| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This command-line option was behaving like the old -require, except that
it did not do Import. In other words, it was loading files without
respecting the loadpath. Now it behaves exactly like Require, while
-require now behaves like Require Import.
This patch also removes Library.require_library_from_file and all its
dependencies, since they are no longer used inside Coq.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
with Enrico.
|
| | | |
|
| | |
| |
| |
| |
| | |
I do not think that this information is worth displaying without
the verbose flag.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Indeed, the name of a bound variable was lost when unifying under a Prod in
evarconv.
The error message for "Unable to satisfy the following constraints" is
still to be improved though.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
|
| | |
| |
| |
| | |
Fixes #4139 (Not_found exception with Require in modules).
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Since Guillaume's, launching coqtop without -native-compiler and call
native_compute would mean recompiling silently all dependencies, even if they
had been precompiled (e.g. the stdlib).
The new semantics is that -native-compiler disables separate compilation of the
current library, but still tries to load precompiled dependencies. If loading
fails when the flag is on, coqtop stays silent.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.
2) Do not remove non-recursive variables when computing minimal levels of inductives.
3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.
4) We correctly solve the recursive equations taking into account the
user-declared level.
|
| | | |
|
| | |
| |
| |
| | |
They appear as axioms of the form `Foo is positive`.
|
| | |
| |
| |
| | |
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.
|
| | |\
| |/
|/| |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| |/ |
|
| |
|
|
| |
Wrong handling of algebraic universes that have upper bounds.
|
| |
|
|
|
|
| |
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Note that this does not prevent using native_compute, but it will force
on-the-fly recompilation of dependencies whenever it is used.
Precompilation is enabled for the standard library, assuming native
compilation was enabled at configuration time.
If native compilation was disabled at configuration time, native_compute
falls back to vm_compute.
Failure to precompile is a hard error, since it is now explicitly required
by the user.
|
| |
|
|
|
|
| |
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
| |
|
|
|
| |
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
| |
|
|
| |
libraries at once (see #4193).
|
| |
|
|
| |
has a strict upper bound.
|
| |
|
|
|
| |
Without this commit, passing "-R theories Coq" to "coqtop -nois" has no
effect since "-Q theories Coq" has already been done implicitly.
|
| | |
|
| |
|
|
|
| |
Also removed the require function it was using, as it is absent from the
remaining of the code.
|
| | |
|
| |
|
|
|
|
|
|
| |
The new behaviour is simple: either a path is in the loadpaths or it is not.
No more wild expansions of paths!
This should not affect -R and -Q, but it does change the semantics of -I -as.
Still, there are no more users of it and it only does so in a subtle way.
|
| | |
|
| | |
|
| |
|
|
| |
It is still present in the libstack, though.
|
| |
|
|
|
| |
We explicit the fact that we only need the name of the library in most of the
summaries.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
| |
|
|
|
| |
Workers send back incomplete system states (only the proof part).
Such part must include the meta/evar counter.
|
| |
|
|
| |
[compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq].
|
| | |
|
| |
|
|
| |
(thanks to Enrico for noticing a bug).
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
Instead of registering all the transitive dependencies of a term in one go,
we rather recursively build the graph of direct dependencies of this term.
This is finer-grained and offers a better API.
The traversal now uses the standard term fold operation, and also registers
inductives and constructors encountered in the traversal.
|
| | |
|
| | |
|
| | |
|
| | |
|
Guillaume Melquiond
Arnaud Spiwack
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
mlasson
Matthieu Sozeau
Enrico Tassi
Thomas Sibut-Pinote
Matthieu Sozeau