| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
| |
|
|
|
|
|
|
|
|
|
| |
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
| |\ |
|
| | | |
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\ \ \ |
|
| |\ \ \ \
| |_|_|/
|/| | | |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| | |_|_|_|/ / /
|/| | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
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.
|
| | |_|/ / / /
|/| | | | |
| | | | | |
| | | | | |
| | | | | | |
This simplifies the representation of values, and brings it closer to
the ones of the native compiler.
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | |/ / / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
`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.
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| |_|_|_|/
|/| | | |
| | | | | |
get_lexer_state.
|
| | |_|_|/
|/| | | |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Otherwise it is possible to detect errors that are not fixed by git
rebase since that works per-commit.
|
| | | | |/ / |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| |_|_|_|/ /
|/| | | | | |
|
| | |_|_|/ /
|/| | | |
| | | | |
| | | | |
| | | | | |
Remove the mention of specific labs (irrelevant for a copyright notice).
Add a mention to represent other contributors and a pointer to CREDITS.
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | | |
That way you can just type [-j] instead of having to remember to add a
space yourself.
|
| | |_|/
|/| | |
|
| | |/
|/| |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
camlp4
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
longer use camlp4.
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | | |
We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
(and alist-alist)
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.
After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.
We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.
|
Emilio Jesus Gallego Arias
Maxime Dénès
Gaëtan Gilbert
Pierre-Marie Pédrot
Enrico Tassi
Théo Zimmermann
Jim Fehrle