| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
supported scenarios.
|
|
Now that the cache is distinct, there should be no nasty side-effects changing
the value of one side while reducing the other.
|
|
|
|
|
|
|
|
This test was actually checking that evar-containing terms were making the
VM fail. Obviously this is not the case anymore, so the test is now invalid.
|
|
|
|
We simply treat them as as an application of an atom to its instance,
and in the decompilation phase we reconstruct the instance from the stack.
This grants wish BZ#5659.
|
|
Following up on #6791, we remove the option "Tactic Pattern Unification"
|
|
Following up on #6791, we remove the option "Standard Proposition Elimination"
|
|
Following up on #6791, we remove the option "Intuition Iff Unfolding"
|
|
Following up on #6791, we remove the option "Injection L2R Pattern Order".
|
|
|
|
|
|
|
|
Fix new deprecation warnings in the standard library.
|
|
This was decided during the Fall WG (2017).
The aliases that are kept as deprecated are the ones where the difference
is only a prefix becoming a qualified module name.
The intention is to turn the warning for deprecated notations on.
We change the compat version to 8.6 to allow the removal of VOld and V8_5.
|
|
This simplifies the representation of values, and brings it closer to
the ones of the native compiler.
|
|
|
|
|
|
|
|
|
|
Example not yet fixed by this patch:
```
Definition u : Type.
Definition m : Type.
exact nat.
Defined.
exact bool.
Defined.
```
|
|
|
|
|
|
|
|
Noticed by Sigurd Schneider.
|
|
|
|
|
|
|
|
|
|
|
|
coq/coq#6511 contains EConstr-related changes.
|
|
Trivial commit.
|
|
`Drop` is implemented using exceptions-as-control flow, so the
toplevel state gets corrupted as `do_vernac` will never return when
`Drop` occurs in the input.
The right fix would be to remove `Drop` from the vernacular and make
it a toplevel-only command, but meanwhile we can just patch the state
in the exception handler.
We also need to keep the global state in `Coqloop` as the main
`coqtop` entry point won't be called by `go ()`.
Fixes #6872.
|
|
|
|
|
|
We first load the file, then we print it as a post-processing
step. This is both more flexible and clearer.
We also refactor the comments handling to minimize the logic that is
living in the Lexer. Indeed, the main API is now living in the
printer, and complex interactions with the state are not possible
anymore, including the removal of messing with low-level summary and
state setting!
|
|
We test the 3 possible scenarios. A more complete test would also
involved fake_ide.
c.f. #6793
|
|
Parsing in `VernacLoad` was broken for a while, but the situation has
improved by miscellaneous refactoring.
However, we still cannot support `Load` properly when proofs are
crossing file boundaries. So in this patch we do two things:
- We check for supported scenarios [no proofs open at `Load` entry/exit]
- Remove the hack in `toplevel` so the behavior of `Load` is
consistent between `coqide`/`coqc`.
We close #5053 as its main bug was fixed by the main toplevel
refactoring and the remaining cases are documented now.
|
|
This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.
The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.
We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.
In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.
Also, the new return type of `Pretyping.understand` should undergo
careful review.
We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.
Some TODOs are:
- impargs was calling whd_all, the Econstr equivalent can be either
+ Reductionops.whd_all [which does refolding and no sharing]
+ Reductionops.clos_whd_flags with all as a flag.
|
|
|
|
|
|
|
|
|
|
We fix as suggested by @JasonGross by reading file names from the
_CoqProject when coq_makefile was invoked with one.
I made coqdep only look at the .v files from _CoqProject because it's
easier this way. Since we're going through the _CoqProject parser we
could have coqdep understand more of it but let's leave that to
another PR (and maybe someone else).
Some projects pass vfiles on the command line, we keep the list of
these files to pass them to coqdep via command line even when there is
a _CoqProject.
Multiple project files is probably broken.
|
|
|
|
|
