| Age | Commit message (Collapse) | Author |
|---|
|
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 evar counter has been moved from Evarutil to Evd, and all functions in
Evarutil now go through a dedicated primitive to create a fresh evar from
an evarmap.
|
|
|
|
(thanks to coq-club, Sep 2015).
|
|
|
|
|
|
A term was reduced in an improper environment.
|
|
|
|
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.
|
|
|
|
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.
|
|
Now distinguishes between bound modules (Top#X) and submodules (Top.X).
Could be useful for the regular printer as well (e.g. in error messages), but I
don't know what the compatibility constraints are, so leaving it as it is for
now.
|
|
(Fix bug #4348)
|
|
|
