| Age | Commit message (Collapse) | Author |
|---|
|
We are forced to declare universes that are global and appear in the
local constraints as we start from an empty universe graph.
|
|
|
|
|
|
|
|
|
|
There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.
|
|
in the loadpath.
This patch causes a bit of code duplication (because of the .coq suffix
added to state files) but it makes it clear which part of the code is
looking up files in the loadpath and for what purpose. Also it makes the
interface of System.extern_intern and System.raw_extern_intern much saner.
|
|
The single remaining use is in library/states.ml. This use should be
reviewed, as it is most certainly broken.
The other uses of Loadpath.get_paths did not disappear by miracle though.
They were replaced by a new function Loadpath.locate_file which factors
all the uses of the function. This function should not be used as it is as
broken as Loadpath.get_paths, by definition.
Vernac.load_vernac now takes a complete path rather than looking up for
the file. That is the way it was used most of the time, so the lookup was
unnecessary. For instance, Vernac.compile was calling Library.start_library
which already expected a complete path.
Another consequence is that System.find_file_in_path is almost no longer
used (except for Loadpath.locate_file, obviously). The two remaining uses
are System.intern_state (used by States.intern_state, cf above) and
Mltop.dir_ml_load for dynamically loading compiled .ml files.
|
|
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].
|
|
|
