| Commit message (Collapse) | Author | Age |
|\ |
|
| | |
|
| |
| |
| |
| |
| |
| | |
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
| |
| |
| |
| |
| |
| |
| |
| | |
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
| |
| |
| |
| |
| |
| | |
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
|/ |
|
|\ |
|
|\ \ |
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.
This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|\ \ |
|
| | |
| | |
| | |
| | | |
Was broken since 8.6.
|
| |/
|/| |
|
| |
| |
| |
| |
| |
| |
| |
| | |
We preserve the level instead of resetting it at level 0.
Probably it would be the same as giving level ltop since Tacexp
apparently comes only from using a tactic in an Ltac "let", which is
where I observed a problem.
|
| |
| |
| |
| |
| | |
This is to avoid excessive parentheses, in particular when printing
"constr:()" in "Print Ltac f".
|
|/ |
|
|\ |
|
| |
| |
| |
| | |
We do up to `Term` which is the main bulk of the changes.
|
|/
|
|
| |
Adding a file fixing #5996 and which uses this feature.
|
|\ |
|
|\ \ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We do it so as to preserve non-focussing semantics for non-focussing
generic arguments.
This assumes that the code treats them consistently, which is not
enforced statically, but which is reasonable in the sense that when we
need a context for printing, we have no other choice as needing a
context and we needed one also at interpretation time.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This concerns pr_value and message_of_value.
This has a few consequences. For instance, no more ad hoc message "a
term" or "a tactic", when not enough information is available for
printing, one gets a generic message "a value of type foobar".
But we also have more printers, satisfying e.g. request #5786.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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".
|
| | | |
|
| | | |
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In Tactic Notation and TACTIC EXTEND, when an argument not ending with
"_list_sep" was given with a separator, the separator was silently
ignored.
Now:
- we take it into account if it is a list (i.e. ending with "_list"), as if
"_list_sep" was given, since after all, the "_sep" is useless in the name.
- we fail if there is a separator but it is not a "_list" or "_list_sep".
|
| |
| |
| |
| |
| |
| | |
We fix by interpreting the pattern in "change pat with term" in strict
mode by using the same interning code as for "match goal" (even if the
pattern is dropped afterwards).
|
|\ \ |
|
|\ \ \
| |_|/
|/| | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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 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.
|
|\ |
|
|\ \
| | |
| | |
| | | |
Morphism` forms.
|
|\ \ \ |
|
| |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| |
| | |
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
|
|\ \ |
|
| | | |
|
| |/
|/|
| |
| |
| | |
For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.
|
|\ \ |
|
| | | |
|
| | |
| | |
| | |
| | |
| | | |
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).
|
| | |
| | |
| | |
| | | |
This commit also fixes range selectors being incorrectly displayed.
|
| |/
| |
| |
| |
| |
| |
| | |
Augment the "Illegal tactic application" error message with the number
of extra arguments passed.
Fixes BZ#5753.
|
| |
| |
| |
| |
| | |
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.
|