| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | | |
Replaced by ident_decl in #688.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to
put any pattern in binders, prefixed by a quote."] its current
placement as well as the hook don't make a lot of sense.
In particular, they prevent parts of Coq working without linking the
parser.
To this purpose, we need to consolidate the `Constrexpr`
utilities. While we are at it we do so and remove the `Topconstr`
module which is fully redundant with `Constrexpr_ops`.
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.
However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.
Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.
We also refactor travis to test more lablgtk versions.
We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.
Fixes #6140.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | |/
|/|
| |
| | |
We do up to `Term` which is the main bulk of the changes.
|
| |\ \
| | |
| | |
| | | |
rules
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The model provides three kinds of printers depending on whether the
printer needs a context, and, if yes if it supports levels. In the
latter case, it takes defaults levels for printing when in a
surrounded context (lconstr style) and for printing when not in a
surrounded context (constr style).
This model preserves the 8.7 focussing semantics of "idtac"
(i.e. focussing only when an env is needed) but it also shows that the
semantics of "idtac", which focusses the goal depending on the type of
its arguments, is a bit ad hoc to understand.
See discussion at PR#6047
"https://github.com/coq/coq/pull/6047#discussion_r148278454".
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
We can now place most of intf modules just after `Libnames/Globnames`
which is quite low on the hierarchy.
A exception is `Vernacexpr` which still depends on `Extend` and
`GOptions`.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Originally, it was not possible to define a new vernacular command
in the following way:
VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
[ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ]
END
because "loc : Loc.t" was not bound.
This commit fixes that, i.e. the location of the custom Vernacular command
(within *.v file) is made available as "loc" variable bound on the right side
of "->" .
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
| |/
|
|
|
| |
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We make Vernacentries.interp functional wrt state, and thus remove
state-handling from `Future`. Now, a future needs a closure if it
wants to preserve state.
Consequently, `Vernacentries.interp` takes a state, and returns the
new one.
We don't explicitly thread the state in the STM yet, instead, we
recover the state that was used before and pass it explicitly to
`interp`.
I have tested the commit with the files in interactive, but we aware
that some new bugs may appear or old ones be made more apparent.
However, I am confident that this step will improve our understanding
of bugs.
In some cases, we perform a bit more summary wrapping/unwrapping. This
will go away in future commits; informal timings for a full make:
- master:
real 2m11,027s
user 8m30,904s
sys 1m0,000s
- no_futures:
real 2m8,474s
user 8m34,380s
sys 0m59,156s
|
| |
|
|
|
| |
We still don't thread the state there, but this is a start of the
needed infrastructure.
|
| |
|
|
|
|
|
|
|
| |
We interpret meta-commands directly, instead of going by an
intermediate "classifier step".
The code could still use some further refactoring, in particular, the
`part_of_script` bit is a bit strange likely coming from some special
treatment of `VtMeta` in the `query` call, and should go away.
|
| |
|
|
|
|
|
|
|
|
| |
The vernacular classifier has a current special case for "Undo" like
commands, as it needs access to the document structure in order to
produce the proper "VtBack" classification, however the classifier is
defined before the document is.
We introduce a new delegation status `VtMeta` that allows us to
interpreted such commands outside the classifier itself.
|
| |
|
|
|
|
|
|
|
| |
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.
For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.
Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When a context variable x is of the form "x := body : Z",
romega is now made aware of this body. Technically, we reify an equation
x = body, and push a corresponding (eq_refl x) as argument of the
final do_omega.
See also the previous commit adding this same feature to omega
(fixing bug 142).
|
| | | |
|
| |/
|
|
|
| |
For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| |/
|
|
|
| |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| | |
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
| |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| |\
| |
| |
| | |
top of the linking chain.
|
| |\ \
| | |
| | |
| | | |
from location in file
|
| |\ \ \ |
|
| | | | | |
|
| | |/ / |
|
| |/ /
| |
| |
| |
| | |
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
Maxime Dénès
Emilio Jesus Gallego Arias
Gaëtan Gilbert
Hugo Herbelin
Matej Košík
Pierre Letouzey
Pierre-Marie Pédrot
Matthieu Sozeau
Guillaume Melquiond