| 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.
|
|
Remove predicative flag and adapt to new invariant where every universe
must be declared, ensuring it is >= Set, safe_repr is not necessary
anymore.
|
|
declare new universes (e.g. with).
|
|
|
|
|
|
|
|
|
|
Rechecking applications built by evarconv's imitation.
|
|
|
|
This fixes a bug in proofgeneral. PG will now diplay this message
eagerly. Otherwise since they appear before the goal, they are
considered outdated and not displayed.
|
|
So that they display in response buffer.
|
|
Incidentally made writing style in CoqIDE chapter more homogeneous.
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
(thanks to coq-club, Sep 2015).
|
|
|
|
|
|
A term was reduced in an improper environment.
|
|
|
|
|
|
|
|
with Enrico.
|
|
in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.
As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
|
|
Auto_ind_decl over the internal lemmas. The schemes are built in the
main process and the internal lemmas are actually already also in the
environment.
|
|
We purge the environment given to the morphism searcher from all dependencies
on the considered variable. I hope it is not too costly.
|
|
The V7 to V8 translator lost part of term annotations.
|
|
On most systems (including Windows, according to the bug report), shortcuts
Ctrl+Alt+Arrows are preempted by the window manager by default. So don't
use them for navigation in Coqide by default. Note that this change only
has an impact when installing on a fresh system; it won't change anything
for existing users.
|
|
|
|
Seems to be morally required since we have the -type-in-type flag.
|
|
|
|
Was left over after Hugo's 9c732a5c878b.
|
|
|
|
and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files"
and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X."
This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
and 69941d4e195650bf59285b897c14d6287defea0f
and e7043eec55085f4101bfb126d8829de6f6086c5a.
Trying to emulate a case sensitive file system on top of a case aware one is
too costly: 3x slowdown when compiling the stdlib or CompCert.
|
|
Substitution on bound modules was incorrectly extended without sequential
composition.
|
|
(Fix bug #4348)
|
|
If it was intentional, please commit again separately.
|
|
The theories/ directory contains no cmi/cmxs files when native_compute is
disabled, so do not try to ship them.
|
|
of temporary hypotheses than 76f27140e6e34 did.
|
|
|
|
Native_compute is not working properly on Windows due to command line size
limitations and the lack of namespaces in OCaml. Using compiler-libs could
solve this, but it is unclear how to ensure stability w.r.t. future versions of
OCaml.
|
|
|
|
of "apply ... in ... as ..." in the context.
Fixing a regression done by 7e00e8d60 and f2130a88e1: when an evar is
created, the statement of the refined hypothesis virtually depends on
the whole context and has to be left at the top.
|
